Metamath Proof Explorer

Theorem minvecolem4b

Description: Lemma for minveco . The convergent point of the Cauchy sequence F is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014) (New usage is discouraged.)

Ref Expression
Hypotheses minveco.x 
|- X = ( BaseSet ` U )
minveco.m 
|- M = ( -v ` U )
minveco.n 
|- N = ( normCV ` U )
minveco.y 
|- Y = ( BaseSet ` W )
minveco.u 
|- ( ph -> U e. CPreHilOLD )
minveco.w 
|- ( ph -> W e. ( ( SubSp ` U ) i^i CBan ) )
minveco.a 
|- ( ph -> A e. X )
minveco.d 
|- D = ( IndMet ` U )
minveco.j 
|- J = ( MetOpen ` D )
minveco.r 
|- R = ran ( y e. Y |-> ( N ` ( A M y ) ) )
minveco.s 
|- S = inf ( R , RR , < )
minveco.f 
|- ( ph -> F : NN --> Y )
minveco.1 
|- ( ( ph /\ n e. NN ) -> ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
Assertion minvecolem4b 
|- ( ph -> ( ( ~~>t ` J ) ` F ) e. X )

Proof

Step Hyp Ref Expression
1 minveco.x 
 |-  X = ( BaseSet ` U )
2 minveco.m 
 |-  M = ( -v ` U )
3 minveco.n 
 |-  N = ( normCV ` U )
4 minveco.y 
 |-  Y = ( BaseSet ` W )
5 minveco.u 
 |-  ( ph -> U e. CPreHilOLD )
6 minveco.w 
 |-  ( ph -> W e. ( ( SubSp ` U ) i^i CBan ) )
7 minveco.a 
 |-  ( ph -> A e. X )
8 minveco.d 
 |-  D = ( IndMet ` U )
9 minveco.j 
 |-  J = ( MetOpen ` D )
10 minveco.r 
 |-  R = ran ( y e. Y |-> ( N ` ( A M y ) ) )
11 minveco.s 
 |-  S = inf ( R , RR , < )
12 minveco.f 
 |-  ( ph -> F : NN --> Y )
13 minveco.1 
 |-  ( ( ph /\ n e. NN ) -> ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
14 phnv 
 |-  ( U e. CPreHilOLD -> U e. NrmCVec )
15 5 14 syl 
 |-  ( ph -> U e. NrmCVec )
16 elin 
 |-  ( W e. ( ( SubSp ` U ) i^i CBan ) <-> ( W e. ( SubSp ` U ) /\ W e. CBan ) )
17 6 16 sylib 
 |-  ( ph -> ( W e. ( SubSp ` U ) /\ W e. CBan ) )
18 17 simpld 
 |-  ( ph -> W e. ( SubSp ` U ) )
19 eqid 
 |-  ( SubSp ` U ) = ( SubSp ` U )
20 1 4 19 sspba 
 |-  ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) -> Y C_ X )
21 15 18 20 syl2anc 
 |-  ( ph -> Y C_ X )
22 1 8 imsxmet 
 |-  ( U e. NrmCVec -> D e. ( *Met ` X ) )
23 15 22 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
24 9 methaus 
 |-  ( D e. ( *Met ` X ) -> J e. Haus )
25 23 24 syl 
 |-  ( ph -> J e. Haus )
26 lmfun 
 |-  ( J e. Haus -> Fun ( ~~>t ` J ) )
27 25 26 syl 
 |-  ( ph -> Fun ( ~~>t ` J ) )
28 1 2 3 4 5 6 7 8 9 10 11 12 13 minvecolem4a 
 |-  ( ph -> F ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) )
29 eqid 
 |-  ( J |`t Y ) = ( J |`t Y )
30 nnuz 
 |-  NN = ( ZZ>= ` 1 )
31 4 fvexi 
 |-  Y e. _V
32 31 a1i 
 |-  ( ph -> Y e. _V )
33 9 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
34 23 33 syl 
 |-  ( ph -> J e. Top )
35 xmetres2 
 |-  ( ( D e. ( *Met ` X ) /\ Y C_ X ) -> ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) )
36 23 21 35 syl2anc 
 |-  ( ph -> ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) )
37 eqid 
 |-  ( MetOpen ` ( D |` ( Y X. Y ) ) ) = ( MetOpen ` ( D |` ( Y X. Y ) ) )
38 37 mopntopon 
 |-  ( ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) -> ( MetOpen ` ( D |` ( Y X. Y ) ) ) e. ( TopOn ` Y ) )
39 36 38 syl 
 |-  ( ph -> ( MetOpen ` ( D |` ( Y X. Y ) ) ) e. ( TopOn ` Y ) )
40 lmcl 
 |-  ( ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) e. ( TopOn ` Y ) /\ F ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) ) -> ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) e. Y )
41 39 28 40 syl2anc 
 |-  ( ph -> ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) e. Y )
42 1zzd 
 |-  ( ph -> 1 e. ZZ )
43 29 30 32 34 41 42 12 lmss 
 |-  ( ph -> ( F ( ~~>t ` J ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) <-> F ( ~~>t ` ( J |`t Y ) ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) ) )
44 eqid 
 |-  ( D |` ( Y X. Y ) ) = ( D |` ( Y X. Y ) )
45 44 9 37 metrest 
 |-  ( ( D e. ( *Met ` X ) /\ Y C_ X ) -> ( J |`t Y ) = ( MetOpen ` ( D |` ( Y X. Y ) ) ) )
46 23 21 45 syl2anc 
 |-  ( ph -> ( J |`t Y ) = ( MetOpen ` ( D |` ( Y X. Y ) ) ) )
47 46 fveq2d 
 |-  ( ph -> ( ~~>t ` ( J |`t Y ) ) = ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) )
48 47 breqd 
 |-  ( ph -> ( F ( ~~>t ` ( J |`t Y ) ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) <-> F ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) ) )
49 43 48 bitrd 
 |-  ( ph -> ( F ( ~~>t ` J ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) <-> F ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) ) )
50 28 49 mpbird 
 |-  ( ph -> F ( ~~>t ` J ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) )
51 funbrfv 
 |-  ( Fun ( ~~>t ` J ) -> ( F ( ~~>t ` J ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) -> ( ( ~~>t ` J ) ` F ) = ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) ) )
52 27 50 51 sylc 
 |-  ( ph -> ( ( ~~>t ` J ) ` F ) = ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) )
53 52 41 eqeltrd 
 |-  ( ph -> ( ( ~~>t ` J ) ` F ) e. Y )
54 21 53 sseldd 
 |-  ( ph -> ( ( ~~>t ` J ) ` F ) e. X )