Metamath Proof Explorer

Theorem minveclem4a

Description: Lemma for minvec . F converges to a point P in Y . (Contributed by Mario Carneiro, 7-May-2014) (Revised by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses minvec.x 
|- X = ( Base ` U )
minvec.m 
|- .- = ( -g ` U )
minvec.n 
|- N = ( norm ` U )
minvec.u 
|- ( ph -> U e. CPreHil )
minvec.y 
|- ( ph -> Y e. ( LSubSp ` U ) )
minvec.w 
|- ( ph -> ( U |`s Y ) e. CMetSp )
minvec.a 
|- ( ph -> A e. X )
minvec.j 
|- J = ( TopOpen ` U )
minvec.r 
|- R = ran ( y e. Y |-> ( N ` ( A .- y ) ) )
minvec.s 
|- S = inf ( R , RR , < )
minvec.d 
|- D = ( ( dist ` U ) |` ( X X. X ) )
minvec.f 
|- F = ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
minvec.p 
|- P = U. ( J fLim ( X filGen F ) )
Assertion minveclem4a 
|- ( ph -> P e. ( ( J fLim ( X filGen F ) ) i^i Y ) )

Proof

Step Hyp Ref Expression
1 minvec.x 
 |-  X = ( Base ` U )
2 minvec.m 
 |-  .- = ( -g ` U )
3 minvec.n 
 |-  N = ( norm ` U )
4 minvec.u 
 |-  ( ph -> U e. CPreHil )
5 minvec.y 
 |-  ( ph -> Y e. ( LSubSp ` U ) )
6 minvec.w 
 |-  ( ph -> ( U |`s Y ) e. CMetSp )
7 minvec.a 
 |-  ( ph -> A e. X )
8 minvec.j 
 |-  J = ( TopOpen ` U )
9 minvec.r 
 |-  R = ran ( y e. Y |-> ( N ` ( A .- y ) ) )
10 minvec.s 
 |-  S = inf ( R , RR , < )
11 minvec.d 
 |-  D = ( ( dist ` U ) |` ( X X. X ) )
12 minvec.f 
 |-  F = ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
13 minvec.p 
 |-  P = U. ( J fLim ( X filGen F ) )
14 ovex 
 |-  ( J fLim ( X filGen F ) ) e. _V
15 14 uniex 
 |-  U. ( J fLim ( X filGen F ) ) e. _V
16 15 snid 
 |-  U. ( J fLim ( X filGen F ) ) e. { U. ( J fLim ( X filGen F ) ) }
17 cphngp 
 |-  ( U e. CPreHil -> U e. NrmGrp )
18 ngpxms 
 |-  ( U e. NrmGrp -> U e. *MetSp )
19 4 17 18 3syl 
 |-  ( ph -> U e. *MetSp )
20 8 1 11 xmstopn 
 |-  ( U e. *MetSp -> J = ( MetOpen ` D ) )
21 19 20 syl 
 |-  ( ph -> J = ( MetOpen ` D ) )
22 21 oveq1d 
 |-  ( ph -> ( J |`t Y ) = ( ( MetOpen ` D ) |`t Y ) )
23 1 11 xmsxmet 
 |-  ( U e. *MetSp -> D e. ( *Met ` X ) )
24 19 23 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
25 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
26 1 25 lssss 
 |-  ( Y e. ( LSubSp ` U ) -> Y C_ X )
27 5 26 syl 
 |-  ( ph -> Y C_ X )
28 eqid 
 |-  ( D |` ( Y X. Y ) ) = ( D |` ( Y X. Y ) )
29 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
30 eqid 
 |-  ( MetOpen ` ( D |` ( Y X. Y ) ) ) = ( MetOpen ` ( D |` ( Y X. Y ) ) )
31 28 29 30 metrest 
 |-  ( ( D e. ( *Met ` X ) /\ Y C_ X ) -> ( ( MetOpen ` D ) |`t Y ) = ( MetOpen ` ( D |` ( Y X. Y ) ) ) )
32 24 27 31 syl2anc 
 |-  ( ph -> ( ( MetOpen ` D ) |`t Y ) = ( MetOpen ` ( D |` ( Y X. Y ) ) ) )
33 22 32 eqtr2d 
 |-  ( ph -> ( MetOpen ` ( D |` ( Y X. Y ) ) ) = ( J |`t Y ) )
34 1 2 3 4 5 6 7 8 9 10 11 12 minveclem3b 
 |-  ( ph -> F e. ( fBas ` Y ) )
35 fgcl 
 |-  ( F e. ( fBas ` Y ) -> ( Y filGen F ) e. ( Fil ` Y ) )
36 34 35 syl 
 |-  ( ph -> ( Y filGen F ) e. ( Fil ` Y ) )
37 1 fvexi 
 |-  X e. _V
38 37 a1i 
 |-  ( ph -> X e. _V )
39 trfg 
 |-  ( ( ( Y filGen F ) e. ( Fil ` Y ) /\ Y C_ X /\ X e. _V ) -> ( ( X filGen ( Y filGen F ) ) |`t Y ) = ( Y filGen F ) )
40 36 27 38 39 syl3anc 
 |-  ( ph -> ( ( X filGen ( Y filGen F ) ) |`t Y ) = ( Y filGen F ) )
41 fgabs 
 |-  ( ( F e. ( fBas ` Y ) /\ Y C_ X ) -> ( X filGen ( Y filGen F ) ) = ( X filGen F ) )
42 34 27 41 syl2anc 
 |-  ( ph -> ( X filGen ( Y filGen F ) ) = ( X filGen F ) )
43 42 oveq1d 
 |-  ( ph -> ( ( X filGen ( Y filGen F ) ) |`t Y ) = ( ( X filGen F ) |`t Y ) )
44 40 43 eqtr3d 
 |-  ( ph -> ( Y filGen F ) = ( ( X filGen F ) |`t Y ) )
45 33 44 oveq12d 
 |-  ( ph -> ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) fLim ( Y filGen F ) ) = ( ( J |`t Y ) fLim ( ( X filGen F ) |`t Y ) ) )
46 xmstps 
 |-  ( U e. *MetSp -> U e. TopSp )
47 19 46 syl 
 |-  ( ph -> U e. TopSp )
48 1 8 istps 
 |-  ( U e. TopSp <-> J e. ( TopOn ` X ) )
49 47 48 sylib 
 |-  ( ph -> J e. ( TopOn ` X ) )
50 fbsspw 
 |-  ( F e. ( fBas ` Y ) -> F C_ ~P Y )
51 34 50 syl 
 |-  ( ph -> F C_ ~P Y )
52 27 sspwd 
 |-  ( ph -> ~P Y C_ ~P X )
53 51 52 sstrd 
 |-  ( ph -> F C_ ~P X )
54 fbasweak 
 |-  ( ( F e. ( fBas ` Y ) /\ F C_ ~P X /\ X e. _V ) -> F e. ( fBas ` X ) )
55 34 53 38 54 syl3anc 
 |-  ( ph -> F e. ( fBas ` X ) )
56 fgcl 
 |-  ( F e. ( fBas ` X ) -> ( X filGen F ) e. ( Fil ` X ) )
57 55 56 syl 
 |-  ( ph -> ( X filGen F ) e. ( Fil ` X ) )
58 filfbas 
 |-  ( ( Y filGen F ) e. ( Fil ` Y ) -> ( Y filGen F ) e. ( fBas ` Y ) )
59 34 35 58 3syl 
 |-  ( ph -> ( Y filGen F ) e. ( fBas ` Y ) )
60 fbsspw 
 |-  ( ( Y filGen F ) e. ( fBas ` Y ) -> ( Y filGen F ) C_ ~P Y )
61 59 60 syl 
 |-  ( ph -> ( Y filGen F ) C_ ~P Y )
62 61 52 sstrd 
 |-  ( ph -> ( Y filGen F ) C_ ~P X )
63 fbasweak 
 |-  ( ( ( Y filGen F ) e. ( fBas ` Y ) /\ ( Y filGen F ) C_ ~P X /\ X e. _V ) -> ( Y filGen F ) e. ( fBas ` X ) )
64 59 62 38 63 syl3anc 
 |-  ( ph -> ( Y filGen F ) e. ( fBas ` X ) )
65 ssfg 
 |-  ( ( Y filGen F ) e. ( fBas ` X ) -> ( Y filGen F ) C_ ( X filGen ( Y filGen F ) ) )
66 64 65 syl 
 |-  ( ph -> ( Y filGen F ) C_ ( X filGen ( Y filGen F ) ) )
67 66 42 sseqtrd 
 |-  ( ph -> ( Y filGen F ) C_ ( X filGen F ) )
68 filtop 
 |-  ( ( Y filGen F ) e. ( Fil ` Y ) -> Y e. ( Y filGen F ) )
69 36 68 syl 
 |-  ( ph -> Y e. ( Y filGen F ) )
70 67 69 sseldd 
 |-  ( ph -> Y e. ( X filGen F ) )
71 flimrest 
 |-  ( ( J e. ( TopOn ` X ) /\ ( X filGen F ) e. ( Fil ` X ) /\ Y e. ( X filGen F ) ) -> ( ( J |`t Y ) fLim ( ( X filGen F ) |`t Y ) ) = ( ( J fLim ( X filGen F ) ) i^i Y ) )
72 49 57 70 71 syl3anc 
 |-  ( ph -> ( ( J |`t Y ) fLim ( ( X filGen F ) |`t Y ) ) = ( ( J fLim ( X filGen F ) ) i^i Y ) )
73 45 72 eqtrd 
 |-  ( ph -> ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) fLim ( Y filGen F ) ) = ( ( J fLim ( X filGen F ) ) i^i Y ) )
74 1 2 3 4 5 6 7 8 9 10 11 minveclem3a 
 |-  ( ph -> ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) )
75 1 2 3 4 5 6 7 8 9 10 11 12 minveclem3 
 |-  ( ph -> ( Y filGen F ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) )
76 30 cmetcvg 
 |-  ( ( ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) /\ ( Y filGen F ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) fLim ( Y filGen F ) ) =/= (/) )
77 74 75 76 syl2anc 
 |-  ( ph -> ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) fLim ( Y filGen F ) ) =/= (/) )
78 73 77 eqnetrrd 
 |-  ( ph -> ( ( J fLim ( X filGen F ) ) i^i Y ) =/= (/) )
79 78 neneqd 
 |-  ( ph -> -. ( ( J fLim ( X filGen F ) ) i^i Y ) = (/) )
80 inss1 
 |-  ( ( J fLim ( X filGen F ) ) i^i Y ) C_ ( J fLim ( X filGen F ) )
81 29 methaus 
 |-  ( D e. ( *Met ` X ) -> ( MetOpen ` D ) e. Haus )
82 23 81 syl 
 |-  ( U e. *MetSp -> ( MetOpen ` D ) e. Haus )
83 20 82 eqeltrd 
 |-  ( U e. *MetSp -> J e. Haus )
84 hausflimi 
 |-  ( J e. Haus -> E* x x e. ( J fLim ( X filGen F ) ) )
85 19 83 84 3syl 
 |-  ( ph -> E* x x e. ( J fLim ( X filGen F ) ) )
86 ssn0 
 |-  ( ( ( ( J fLim ( X filGen F ) ) i^i Y ) C_ ( J fLim ( X filGen F ) ) /\ ( ( J fLim ( X filGen F ) ) i^i Y ) =/= (/) ) -> ( J fLim ( X filGen F ) ) =/= (/) )
87 80 78 86 sylancr 
 |-  ( ph -> ( J fLim ( X filGen F ) ) =/= (/) )
88 n0moeu 
 |-  ( ( J fLim ( X filGen F ) ) =/= (/) -> ( E* x x e. ( J fLim ( X filGen F ) ) <-> E! x x e. ( J fLim ( X filGen F ) ) ) )
89 87 88 syl 
 |-  ( ph -> ( E* x x e. ( J fLim ( X filGen F ) ) <-> E! x x e. ( J fLim ( X filGen F ) ) ) )
90 85 89 mpbid 
 |-  ( ph -> E! x x e. ( J fLim ( X filGen F ) ) )
91 euen1b 
 |-  ( ( J fLim ( X filGen F ) ) ~~ 1o <-> E! x x e. ( J fLim ( X filGen F ) ) )
92 90 91 sylibr 
 |-  ( ph -> ( J fLim ( X filGen F ) ) ~~ 1o )
93 en1b 
 |-  ( ( J fLim ( X filGen F ) ) ~~ 1o <-> ( J fLim ( X filGen F ) ) = { U. ( J fLim ( X filGen F ) ) } )
94 92 93 sylib 
 |-  ( ph -> ( J fLim ( X filGen F ) ) = { U. ( J fLim ( X filGen F ) ) } )
95 80 94 sseqtrid 
 |-  ( ph -> ( ( J fLim ( X filGen F ) ) i^i Y ) C_ { U. ( J fLim ( X filGen F ) ) } )
96 sssn 
 |-  ( ( ( J fLim ( X filGen F ) ) i^i Y ) C_ { U. ( J fLim ( X filGen F ) ) } <-> ( ( ( J fLim ( X filGen F ) ) i^i Y ) = (/) \/ ( ( J fLim ( X filGen F ) ) i^i Y ) = { U. ( J fLim ( X filGen F ) ) } ) )
97 95 96 sylib 
 |-  ( ph -> ( ( ( J fLim ( X filGen F ) ) i^i Y ) = (/) \/ ( ( J fLim ( X filGen F ) ) i^i Y ) = { U. ( J fLim ( X filGen F ) ) } ) )
98 97 ord 
 |-  ( ph -> ( -. ( ( J fLim ( X filGen F ) ) i^i Y ) = (/) -> ( ( J fLim ( X filGen F ) ) i^i Y ) = { U. ( J fLim ( X filGen F ) ) } ) )
99 79 98 mpd 
 |-  ( ph -> ( ( J fLim ( X filGen F ) ) i^i Y ) = { U. ( J fLim ( X filGen F ) ) } )
100 16 99 eleqtrrid 
 |-  ( ph -> U. ( J fLim ( X filGen F ) ) e. ( ( J fLim ( X filGen F ) ) i^i Y ) )
101 13 100 eqeltrid 
 |-  ( ph -> P e. ( ( J fLim ( X filGen F ) ) i^i Y ) )