Theorem projlem25 9205

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 9211.

Hypotheses

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

Assertion

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

Distinct variable groups:   x,y,A   x,z,F,y   z,G

Proof of Theorem projlem25

Step	Hyp	Ref	Expression
1		projlem25.3	. . . 4 |- F e. V
2		visset 1816	. . . 4 |- z e. V
3	1, 2	hlimconv 9054	. . 3 |- (F ~~>v z -> A.w e. RR (0 < w -> E.v e. NN A.u e. NN (v <_ u -> (normh` ((F` u) -h z)) < w)))
4		lelttrt 5535	. . . . . . . . . . . . . . 15 |- (((abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) e. RR /\ (normh` ((F` u) -h z)) e. RR /\ w e. RR) -> (((abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) <_ (normh` ((F` u) -h z)) /\ (normh` ((F` u) -h z)) < w) -> (abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) < w))
5	4	3expa 835	. . . . . . . . . . . . . 14 |- ((((abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) e. RR /\ (normh` ((F` u) -h z)) e. RR) /\ w e. RR) -> (((abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) <_ (normh` ((F` u) -h z)) /\ (normh` ((F` u) -h z)) < w) -> (abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) < w))
6		resubclt 5450	. . . . . . . . . . . . . . . . . 18 |- (((normh` ((F` u) -h A)) e. RR /\ (normh` (z -h A)) e. RR) -> ((normh` ((F` u) -h A)) - (normh` (z -h A))) e. RR)
7		ffvelrn 3820	. . . . . . . . . . . . . . . . . . . 20 |- ((F:NN-->H~ /\ u e. NN) -> (F` u) e. H~)
8	1, 2	hlimseq 9052	. . . . . . . . . . . . . . . . . . . 20 |- (F ~~>v z -> F:NN-->H~)
9	7, 8	sylan 450	. . . . . . . . . . . . . . . . . . 19 |- ((F ~~>v z /\ u e. NN) -> (F` u) e. H~)
10		projlem25.2	. . . . . . . . . . . . . . . . . . . 20 |- A e. H~
11		hvsubclt 8882	. . . . . . . . . . . . . . . . . . . 20 |- (((F` u) e. H~ /\ A e. H~) -> ((F` u) -h A) e. H~)
12	10, 11	mpan2 698	. . . . . . . . . . . . . . . . . . 19 |- ((F` u) e. H~ -> ((F` u) -h A) e. H~)
13		normclt 8986	. . . . . . . . . . . . . . . . . . 19 |- (((F` u) -h A) e. H~ -> (normh` ((F` u) -h A)) e. RR)
14	9, 12, 13	3syl 20	. . . . . . . . . . . . . . . . . 18 |- ((F ~~>v z /\ u e. NN) -> (normh` ((F` u) -h A)) e. RR)
15	1, 2	hlimvec 9053	. . . . . . . . . . . . . . . . . . . 20 |- (F ~~>v z -> z e. H~)
16	15	adantr 391	. . . . . . . . . . . . . . . . . . 19 |- ((F ~~>v z /\ u e. NN) -> z e. H~)
17		hvsubclt 8882	. . . . . . . . . . . . . . . . . . . 20 |- ((z e. H~ /\ A e. H~) -> (z -h A) e. H~)
18	10, 17	mpan2 698	. . . . . . . . . . . . . . . . . . 19 |- (z e. H~ -> (z -h A) e. H~)
19		normclt 8986	. . . . . . . . . . . . . . . . . . 19 |- ((z -h A) e. H~ -> (normh` (z -h A)) e. RR)
20	16, 18, 19	3syl 20	. . . . . . . . . . . . . . . . . 18 |- ((F ~~>v z /\ u e. NN) -> (normh` (z -h A)) e. RR)
21	6, 14, 20	sylanc 473	. . . . . . . . . . . . . . . . 17 |- ((F ~~>v z /\ u e. NN) -> ((normh` ((F` u) -h A)) - (normh` (z -h A))) e. RR)
22	21	recnd 5327	. . . . . . . . . . . . . . . 16 |- ((F ~~>v z /\ u e. NN) -> ((normh` ((F` u) -h A)) - (normh` (z -h A))) e. CC)
23		absclt 6833	. . . . . . . . . . . . . . . 16 |- (((normh` ((F` u) -h A)) - (normh` (z -h A))) e. CC -> (abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) e. RR)
24	22, 23	syl 10	. . . . . . . . . . . . . . 15 |- ((F ~~>v z /\ u e. NN) -> (abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) e. RR)
25		hvsubclt 8882	. . . . . . . . . . . . . . . . 17 |- (((F` u) e. H~ /\ z e. H~) -> ((F` u) -h z) e. H~)
26	25, 9, 16	sylanc 473	. . . . . . . . . . . . . . . 16 |- ((F ~~>v z /\ u e. NN) -> ((F` u) -h z) e. H~)
27		normclt 8986	. . . . . . . . . . . . . . . 16 |- (((F` u) -h z) e. H~ -> (normh` ((F` u) -h z)) e. RR)
28	26, 27	syl 10	. . . . . . . . . . . . . . 15 |- ((F ~~>v z /\ u e. NN) -> (normh` ((F` u) -h z)) e. RR)
29	24, 28	jca 288	. . . . . . . . . . . . . 14 |- ((F ~~>v z /\ u e. NN) -> ((abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) e. RR /\ (normh` ((F` u) -h z)) e. RR))
30	5, 29	sylan 450	. . . . . . . . . . . . 13 |- (((F ~~>v z /\ u e. NN) /\ w e. RR) -> (((abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) <_ (normh` ((F` u) -h z)) /\ (normh` ((F` u) -h z)) < w) -> (abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) < w))
31	30	an1rs 491	. . . . . . . . . . . 12 |- (((F ~~>v z /\ w e. RR) /\ u e. NN) -> (((abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) <_ (normh` ((F` u) -h z)) /\ (normh` ((F` u) -h z)) < w) -> (abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) < w))
32	10	norm3adift 9015	. . . . . . . . . . . . . 14 |- (((F` u) e. H~ /\ z e. H~) -> (abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) <_ (normh` ((F` u) -h z)))
33	32, 9, 16	sylanc 473	. . . . . . . . . . . . 13 |- ((F ~~>v z /\ u e. NN) -> (abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) <_ (normh` ((F` u) -h z)))
34	33	adantlr 395	. . . . . . . . . . . 12 |- (((F ~~>v z /\ w e. RR) /\ u e. NN) -> (abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) <_ (normh` ((F` u) -h z)))
35	31, 34	sylani 466	. . . . . . . . . . 11 |- (((F ~~>v z /\ w e. RR) /\ u e. NN) -> ((((F ~~>v z /\ w e. RR) /\ u e. NN) /\ (normh` ((F` u) -h z)) < w) -> (abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) < w))
36	35	anabsi5 497	. . . . . . . . . 10 |- ((((F ~~>v z /\ w e. RR) /\ u e. NN) /\ (normh` ((F` u) -h z)) < w) -> (abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) < w)
37		projlem23.1	. . . . . . . . . . . . . . 15 |- G = {<.x, y>. | (x e. NN /\ y = (normh` ((F` x) -h A)))}
38	37	projlem23 9203	. . . . . . . . . . . . . 14 |- (u e. NN -> (G` u) = (normh` ((F` u) -h A)))
39	38	opreq1d 3981	. . . . . . . . . . . . 13 |- (u e. NN -> ((G` u) - (normh` (z -h A))) = ((normh` ((F` u) -h A)) - (normh` (z -h A))))
40	39	fveq2d 3734	. . . . . . . . . . . 12 |- (u e. NN -> (abs` ((G` u) - (normh` (z -h A)))) = (abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))))
41	40	breq1d 2634	. . . . . . . . . . 11 |- (u e. NN -> ((abs` ((G` u) - (normh` (z -h A)))) < w <-> (abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) < w))
42	41	ad2antlr 407	. . . . . . . . . 10 |- ((((F ~~>v z /\ w e. RR) /\ u e. NN) /\ (normh` ((F` u) -h z)) < w) -> ((abs` ((G` u) - (normh` (z -h A)))) < w <-> (abs` ((normh` ((F` u) -h A)) - (normh` (z -h A)))) < w))
43	36, 42	mpbird 196	. . . . . . . . 9 |- ((((F ~~>v z /\ w e. RR) /\ u e. NN) /\ (normh` ((F` u) -h z)) < w) -> (abs` ((G` u) - (normh` (z -h A)))) < w)
44	43