Theorem projlem25 5217

Description: Part of Lemma 3.6 of [Beran] p. 101. "The sequence {||yn-x0||} of real numbers converges to the number ||y0-x0||" (here, "y0" is A and "x0" is z). Used by projlem31 5223.

Hypotheses

Ref	Expression
projlem23.1	|- G = {<.x, y>. | (x e. NN /\ y = (norm` ((F` x) -v A)))}
projlem25.2	|- A e. H~
projlem25.3	|- F e. V

Assertion

Ref	Expression
projlem25	|- (F ~~>v z -> G ~~> (norm` (z -v A)))

Distinct variable group(s):   x,y,A   x,z,F,y   z,G

Proof of Theorem projlem25

Step	Hyp	Ref	Expression
1		projlem25.3	. . . . . 6 |- F e. V
2		visset 1350	. . . . . 6 |- z e. V
3	1, 2	hlimseq 5109	. . . . 5 |- (F ~~>v z -> F:NN-->H~)
4		projlem23.1	. . . . . 6 |- G = {<.x, y>. | (x e. NN /\ y = (norm` ((F` x) -v A)))}
5		projlem25.2	. . . . . 6 |- A e. H~
6	4, 5	projlem24 5216	. . . . 5 |- (F:NN-->H~ -> G:NN-->CC)
7	3, 6	syl 12	. . . 4 |- (F ~~>v z -> G:NN-->CC)
8	1, 2	hlimvec 5110	. . . . . . 7 |- (F ~~>v z -> z e. H~)
9	8, 5	jctir 241	. . . . . 6 |- (F ~~>v z -> (z e. H~ /\ A e. H~))
10		hvsubclt 4998	. . . . . 6 |- ((z e. H~ /\ A e. H~) -> (z -v A) e. H~)
11		normclt 5076	. . . . . 6 |- ((z -v A) e. H~ -> (norm` (z -v A)) e. RR)
12	9, 10, 11	3syl 21	. . . . 5 |- (F ~~>v z -> (norm` (z -v A)) e. RR)
13	12	recnd 4099	. . . 4 |- (F ~~>v z -> (norm` (z -v A)) e. CC)
14	7, 13	jca 236	. . 3 |- (F ~~>v z -> (G:NN-->CC /\ (norm` (z -v A)) e. CC))
15	1, 2	hlimconv 5111	. . . 4 |- (F ~~>v z -> A.w e. RR (0 < w -> E.v e. NN A.u e. NN (v <_ u -> (norm` ((F` u) -v z)) < w)))
16		lelttrt 4289	. . . . . . . . . . . . . . . 16 |- (((abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) e. RR /\ (norm` ((F` u) -v z)) e. RR /\ w e. RR) -> (((abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) <_ (norm` ((F` u) -v z)) /\ (norm` ((F` u) -v z)) < w) -> (abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) < w))
17	16	3expa 612	. . . . . . . . . . . . . . 15 |- ((((abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) e. RR /\ (norm` ((F` u) -v z)) e. RR) /\ w e. RR) -> (((abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) <_ (norm` ((F` u) -v z)) /\ (norm` ((F` u) -v z)) < w) -> (abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) < w))
18		resubclt 4173	. . . . . . . . . . . . . . . . . . 19 |- (((norm` ((F` u) -v A)) e. RR /\ (norm` (z -v A)) e. RR) -> ((norm` ((F` u) -v A)) - (norm` (z -v A))) e. RR)
19		ffvrn 2890	. . . . . . . . . . . . . . . . . . . . 21 |- ((F:NN-->H~ /\ u e. NN) -> (F` u) e. H~)
20	19, 3	sylan 343	. . . . . . . . . . . . . . . . . . . 20 |- ((F ~~>v z /\ u e. NN) -> (F` u) e. H~)
21		hvsubclt 4998	. . . . . . . . . . . . . . . . . . . . 21 |- (((F` u) e. H~ /\ A e. H~) -> ((F` u) -v A) e. H~)
22	5, 21	mpan2 519	. . . . . . . . . . . . . . . . . . . 20 |- ((F` u) e. H~ -> ((F` u) -v A) e. H~)
23		normclt 5076	. . . . . . . . . . . . . . . . . . . 20 |- (((F` u) -v A) e. H~ -> (norm` ((F` u) -v A)) e. RR)
24	20, 22, 23	3syl 21	. . . . . . . . . . . . . . . . . . 19 |- ((F ~~>v z /\ u e. NN) -> (norm` ((F` u) -v A)) e. RR)
25	8	adantr 306	. . . . . . . . . . . . . . . . . . . 20 |- ((F ~~>v z /\ u e. NN) -> z e. H~)
26	5, 10	mpan2 519	. . . . . . . . . . . . . . . . . . . 20 |- (z e. H~ -> (z -v A) e. H~)
27	25, 26, 11	3syl 21	. . . . . . . . . . . . . . . . . . 19 |- ((F ~~>v z /\ u e. NN) -> (norm` (z -v A)) e. RR)
28	18, 24, 27	sylanc 361	. . . . . . . . . . . . . . . . . 18 |- ((F ~~>v z /\ u e. NN) -> ((norm` ((F` u) -v A)) - (norm` (z -v A))) e. RR)
29	28	recnd 4099	. . . . . . . . . . . . . . . . 17 |- ((F ~~>v z /\ u e. NN) -> ((norm` ((F` u) -v A)) - (norm` (z -v A))) e. CC)
30		absclt 4848	. . . . . . . . . . . . . . . . 17 |- (((norm` ((F` u) -v A)) - (norm` (z -v A))) e. CC -> (abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) e. RR)
31	29, 30	syl 12	. . . . . . . . . . . . . . . 16 |- ((F ~~>v z /\ u e. NN) -> (abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) e. RR)
32		hvsubclt 4998	. . . . . . . . . . . . . . . . . 18 |- (((F` u) e. H~ /\ z e. H~) -> ((F` u) -v z) e. H~)
33	32, 20, 25	sylanc 361	. . . . . . . . . . . . . . . . 17 |- ((F ~~>v z /\ u e. NN) -> ((F` u) -v z) e. H~)
34		normclt 5076	. . . . . . . . . . . . . . . . 17 |- (((F` u) -v z) e. H~ -> (norm` ((F` u) -v z)) e. RR)
35	33, 34	syl 12	. . . . . . . . . . . . . . . 16 |- ((F ~~>v z /\ u e. NN) -> (norm` ((F` u) -v z)) e. RR)
36	31, 35	jca 236	. . . . . . . . . . . . . . 15 |- ((F ~~>v z /\ u e. NN) -> ((abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) e. RR /\ (norm` ((F` u) -v z)) e. RR))
37	17, 36	sylan 343	. . . . . . . . . . . . . 14 |- (((F ~~>v z /\ u e. NN) /\ w e. RR) -> (((abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) <_ (norm` ((F` u) -v z)) /\ (norm` ((F` u) -v z)) < w) -> (abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) < w))
38	37	an1rs 373	. . . . . . . . . . . . 13 |- (((F ~~>v z /\ w e. RR) /\ u e. NN) -> (((abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) <_ (norm` ((F` u) -v z)) /\ (norm` ((F` u) -v z)) < w) -> (abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) < w))
39	5	norm3adift 5098	. . . . . . . . . . . . . . 15 |- (((F` u) e. H~ /\ z e. H~) -> (abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) <_ (norm` ((F` u) -v z)))
40	39, 20, 25	sylanc 361	. . . . . . . . . . . . . 14 |- ((F ~~>v z /\ u e. NN) -> (abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) <_ (norm` ((F` u) -v z)))
41	40	adantlr 310	. . . . . . . . . . . . 13 |- (((F ~~>v z /\ w e. RR) /\ u e. NN) -> (abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) <_ (norm` ((F` u) -v z)))
42	38, 41	sylani 356	. . . . . . . . . . . 12 |- (((F ~~>v z /\ w e. RR) /\ u e. NN) -> ((((F ~~>v z /\ w e. RR) /\ u e. NN) /\ (norm` ((F` u) -v z)) < w) -> (abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) < w))
43	42	anabsi5 377	. . . . . . . . . . 11 |- ((((F ~~>v z /\ w e. RR) /\ u e. NN) /\ (norm` ((F` u) -v z)) < w) -> (abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) < w)
44	4	projlem23 5215	. . . . . . . . . . . . . . 15 |- (u e. NN -> (G` u) = (norm` ((F` u) -v A)))
45	44	opreq1d 3012	. . . . . . . . . . . . . 14 |- (u e. NN -> ((G` u) - (norm` (z -v A))) = ((norm` ((F` u) -v A)) - (norm` (z -v A))))
46	45	fveq2d 2836	. . . . . . . . . . . . 13 |- (u e. NN -> (abs` ((G` u) - (norm` (z -v A)))) = (abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))))
47	46	breq1d 2071	. . . . . . . . . . . 12 |- (u e. NN -> ((abs` ((G` u) - (norm` (z -v A)))) < w <-> (abs` ((norm` ((F` u) -v A)) - (norm` (z -v A)))) < w))
48	47	ad2antlr 321	. . . . . . . . . . 11 |- ((((F ~~>v z /\ w e. RR) /\ u e. NN) /\ (norm` ((F` u) -v z)) < w) -> ((abs` ((G` u) - (norm` (z -v A)))) < w <-> (abs` ((norm` ((F` u) -v A)) - (