HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem projlem26 9127
Description: Part of Lemma 3.6 of [Beran] p. 101. The real sequence G (Beran's "{||yn-x0||}") converges to the infimum of norms. Used by projlem31 9132.
Hypotheses
Ref Expression
projlem26.1 |- A e. H~
projlem26.2 |- H e. CH
projlem26.3 |- S = {u e. RR | E.v e. H u = -u(normh` (v -h A))}
projlem26.4 |- R = -usup(S, RR, < )
projlem26.5 |- (ph <-> (F:NN-->H /\ A.w e. NN ((R - (1 / w)) < (normh` ((F` w) -h A)) /\ (normh` ((F` w) -h A)) < (R + (1 / w)))))
projlem26.6 |- G = {<.x, y>. | (x e. NN /\ y = (normh` ((F` x) -h A)))}
Assertion
Ref Expression
projlem26 |- (ph -> G ~~> R)
Distinct variable groups:   w,u,v,x,y,A   w,F,x,y   w,R   ph,x   u,H,v
Proof of Theorem projlem26
StepHypRef Expression
1 gt0ne0t 5592 . . . . . . . . 9 |- ((z e. RR /\ 0 < z) -> z =/= 0)
2 rerecclt 5759 . . . . . . . . 9 |- ((z e. RR /\ z =/= 0) -> (1 / z) e. RR)
31, 2syldan 467 . . . . . . . 8 |- ((z e. RR /\ 0 < z) -> (1 / z) e. RR)
4 arch 6018 . . . . . . . 8 |- ((1 / z) e. RR -> E.f e. NN (1 / z) < f)
53, 4syl 10 . . . . . . 7 |- ((z e. RR /\ 0 < z) -> E.f e. NN (1 / z) < f)
6 ltrec1t 5836 . . . . . . . . 9 |- (((z e. RR /\ 0 < z) /\ (f e. RR /\ 0 < f)) -> ((1 / z) < f <-> (1 / f) < z))
7 nnret 5877 . . . . . . . . . 10 |- (f e. NN -> f e. RR)
8 nngt0t 5894 . . . . . . . . . 10 |- (f e. NN -> 0 < f)
97, 8jca 288 . . . . . . . . 9 |- (f e. NN -> (f e. RR /\ 0 < f))
106, 9sylan2 451 . . . . . . . 8 |- (((z e. RR /\ 0 < z) /\ f e. NN) -> ((1 / z) < f <-> (1 / f) < z))
1110rexbidva 1652 . . . . . . 7 |- ((z e. RR /\ 0 < z) -> (E.f e. NN (1 / z) < f <-> E.f e. NN (1 / f) < z))
125, 11mpbid 195 . . . . . 6 |- ((z e. RR /\ 0 < z) -> E.f e. NN (1 / f) < z)
1312adantl 388 . . . . 5 |- ((ph /\ (z e. RR /\ 0 < z)) -> E.f e. NN (1 / f) < z)
14 lerect 5833 . . . . . . . . . . . . . . . . . . . . 21 |- (((f e. RR /\ 0 < f) /\ (g e. RR /\ 0 < g)) -> (f <_ g <-> (1 / g) <_ (1 / f)))
15 nnret 5877 . . . . . . . . . . . . . . . . . . . . . 22 |- (g e. NN -> g e. RR)
16 nngt0t 5894 . . . . . . . . . . . . . . . . . . . . . 22 |- (g e. NN -> 0 < g)
1715, 16jca 288 . . . . . . . . . . . . . . . . . . . . 21 |- (g e. NN -> (g e. RR /\ 0 < g))
1814, 9, 17syl2an 454 . . . . . . . . . . . . . . . . . . . 20 |- ((f e. NN /\ g e. NN) -> (f <_ g <-> (1 / g) <_ (1 / f)))
1918ancoms 436 . . . . . . . . . . . . . . . . . . 19 |- ((g e. NN /\ f e. NN) -> (f <_ g <-> (1 / g) <_ (1 / f)))
20193adant3 797 . . . . . . . . . . . . . . . . . 18 |- ((g e. NN /\ f e. NN /\ z e. RR) -> (f <_ g <-> (1 / g) <_ (1 / f)))
21 lelttrt 5496 . . . . . . . . . . . . . . . . . . . . 21 |- (((1 / g) e. RR /\ (1 / f) e. RR /\ z e. RR) -> (((1 / g) <_ (1 / f) /\ (1 / f) < z) -> (1 / g) < z))
2221exp3a 375 . . . . . . . . . . . . . . . . . . . 20 |- (((1 / g) e. RR /\ (1 / f) e. RR /\ z e. RR) -> ((1 / g) <_ (1 / f) -> ((1 / f) < z -> (1 / g) < z)))
23 rerecclt 5759 . . . . . . . . . . . . . . . . . . . . 21 |- ((f e. RR /\ f =/= 0) -> (1 / f) e. RR)
24 nnne0t 5897 . . . . . . . . . . . . . . . . . . . . 21 |- (f e. NN -> f =/= 0)
2523, 7, 24sylanc 471 . . . . . . . . . . . . . . . . . . . 20 |- (f e. NN -> (1 / f) e. RR)
2622, 25syl3an2 858 . . . . . . . . . . . . . . . . . . 19 |- (((1 / g) e. RR /\ f e. NN /\ z e. RR) -> ((1 / g) <_ (1 / f) -> ((1 / f) < z -> (1 / g) < z)))
27 rerecclt 5759 . . . . . . . . . . . . . . . . . . . 20 |- ((g e. RR /\ g =/= 0) -> (1 / g) e. RR)
28 nnne0t 5897 . . . . . . . . . . . . . . . . . . . 20 |- (g e. NN -> g =/= 0)
2927, 15, 28sylanc 471 . . . . . . . . . . . . . . . . . . 19 |- (g e. NN -> (1 / g) e. RR)
3026, 29syl3an1 857 . . . . . . . . . . . . . . . . . 18 |- ((g e. NN /\ f e. NN /\ z e. RR) -> ((1 / g) <_ (1 / f) -> ((1 / f) < z -> (1 / g) < z)))
3120, 30sylbid 203 . . . . . . . . . . . . . . . . 17 |- ((g e. NN /\ f e. NN /\ z e. RR) -> (f <_ g -> ((1 / f) < z -> (1 / g) < z)))
3231com23 32 . . . . . . . . . . . . . . . 16 |- ((g e. NN /\ f e. NN /\ z e. RR) -> ((1 / f) < z -> (f <_ g -> (1 / g) < z)))
3332imp3a 361 . . . . . . . . . . . . . . 15 |- ((g e. NN /\ f e. NN /\ z e. RR) -> (((1 / f) < z /\ f <_ g) -> (1 / g) < z))
34333exp 830 . . . . . . . . . . . . . 14 |- (g e. NN -> (f e. NN -> (z e. RR -> (((1 / f) < z /\ f <_ g) -> (1 / g) < z))))
3534com13 33 . . . . . . . . . . . . 13 |- (z e. RR -> (f e. NN -> (g e. NN -> (((1 / f) < z /\ f <_ g) -> (1 / g) < z))))
3635ad2antrl 406 . . . . . . . . . . . 12 |- ((ph /\ (z e. RR /\ 0 < z)) -> (f e. NN -> (g e. NN -> (((1 / f) < z /\ f <_ g) -> (1 / g) < z))))
3736imp31 362 . . . . . . . . . . 11 |- ((((ph /\ (z e. RR /\ 0 < z)) /\ f e. NN) /\ g e. NN) -> (((1 / f) < z /\ f <_ g) -> (1 / g) < z))
38 axlttrn 5476 . . . . . . . . . . . . . . . 16 |- (((abs` ((normh` ((F` g) -h A)) - R)) e. RR /\ (1 / g) e. RR /\ z e. RR) -> (((abs` ((normh` ((F` g) -h A)) - R)) < (1 / g) /\ (1 / g) < z) -> (abs` ((normh` ((F` g) -h A)) - R)) < z))
39383expa 831 . . . . . . . . . . . . . . 15 |- ((((abs` ((normh` ((F` g) -h A)) - R)) e. RR /\ (1 / g) e. RR) /\ z e. RR) -> (((abs` ((normh` ((F` g) -h A)) - R)) < (1 / g) /\ (1 / g) < z) -> (abs` ((normh` ((F` g) -h A)) - R)) < z))
4039exp3a 375 . . . . . . . . . . . . . 14 |- ((((abs` ((normh` ((F` g) -h A)) - R)) e. RR /\ (1 / g) e. RR) /\ z e. RR) -> ((abs` ((normh` ((F` g) -h A)) - R)) < (1 / g) -> ((1 / g) < z -> (abs` ((normh` ((F` g) -h A)) - R)) < z)))
41 ffvelrn 3799 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F:NN-->H /\ g e. NN) -> (F` g) e. H)
42 projlem26.5 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (ph <-> (F:NN-->H /\ A.w e. NN ((R - (1 / w)) < (normh` ((F` w) -h A)) /\ (normh` ((F` w) -h A)) < (R + (1 / w)))))
4342pm3.26bi 322 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (ph -> F:NN-->H)
4441, 43sylan 448 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((ph /\ g e. NN) -> (F` g) e. H)
45 projlem26.2 . . . . . . . . . . . . . . . . . . . . . . . 24 |- H e. CH
4645chel 9023 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((F` g) e. H -> (F` g) e. H~)
4744, 46syl 10 . . . . . . . . . . . . . . . . . . . . . 22 |- ((ph /\ g e. NN) -> (F` g) e. H~)
48 projlem26.1 . . . . . . . . . . . . . . . . . . . . . 22 |- A e. H~
4947, 48jctir 293 . . . . . . . . . . . . . . . . . . . . 21 |- ((ph /\ g e. NN) -> ((F` g) e. H~ /\ A e. H~))
50 hvsubclt 8808 . . . . . . . . . . . . . . . . . . . . 21 |- (((F` g) e. H~ /\ A e. H~) -> ((F` g) -h A) e. H~)
51 normclt 8912 . . . . . . . . . . . . . . . . . . . . 21 |- (((F` g) -h A) e. H~ -> (normh` ((F` g) -h A)) e. RR)
5249, 50, 513syl 20 . . . . . . . . . . . . . . . . . . . 20 |- ((ph /\ g e. NN) -> (normh` ((F` g) -h A)) e. RR)
53 projlem26.3 . . . . . . . . . . . . . . . . . . . . 21 |- S = {u e. RR | E.v e. H u = -u(normh` (v -h A))}
54 projlem26.4 . . . . . . . . . . . . . . . . . . . . 21 |- R = -usup(S, RR, < )
5548, 45, 53, 54projlem11 9112 . . . . . . . . . . . . . . . . . . . 20 |- R e. RR
5652, 55jctir 293 . . . . . . . . . . . . . . . . . . 19 |- ((ph /\ g e. NN) -> ((normh` ((F` g) -h A)) e. RR /\ R e. RR))
57 resubclt 5410 . . . . . . . . . . . . . . . . . . 19 |- (((normh` ((F` g) -h A)) e. RR /\ R e. RR) -> ((normh` ((F` g) -h A)) - R) e. RR)
5856, 57syl 10 . . . . . . . . . . . . . . . . . 18 |- ((ph /\ g e. NN) -> ((normh` ((F` g) -h A)) - R) e. RR)
5958recnd 5287 . . . . . . . . . . . . . . . . 17 |- ((ph /\ g e. NN) -> ((normh` (