| 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 |
|- ( IndMet ` W ) = ( IndMet ` W ) |
| 20 |
|
eqid |
|- ( SubSp ` U ) = ( SubSp ` U ) |
| 21 |
4 8 19 20
|
sspims |
|- ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) -> ( IndMet ` W ) = ( D |` ( Y X. Y ) ) ) |
| 22 |
15 18 21
|
syl2anc |
|- ( ph -> ( IndMet ` W ) = ( D |` ( Y X. Y ) ) ) |
| 23 |
17
|
simprd |
|- ( ph -> W e. CBan ) |
| 24 |
|
eqid |
|- ( BaseSet ` W ) = ( BaseSet ` W ) |
| 25 |
24 19
|
cbncms |
|- ( W e. CBan -> ( IndMet ` W ) e. ( CMet ` ( BaseSet ` W ) ) ) |
| 26 |
23 25
|
syl |
|- ( ph -> ( IndMet ` W ) e. ( CMet ` ( BaseSet ` W ) ) ) |
| 27 |
22 26
|
eqeltrrd |
|- ( ph -> ( D |` ( Y X. Y ) ) e. ( CMet ` ( BaseSet ` W ) ) ) |
| 28 |
1 2 3 4 5 6 7 8 9 10 11 12 13
|
minvecolem3 |
|- ( ph -> F e. ( Cau ` D ) ) |
| 29 |
1 8
|
imsmet |
|- ( U e. NrmCVec -> D e. ( Met ` X ) ) |
| 30 |
5 14 29
|
3syl |
|- ( ph -> D e. ( Met ` X ) ) |
| 31 |
|
metxmet |
|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) ) |
| 32 |
30 31
|
syl |
|- ( ph -> D e. ( *Met ` X ) ) |
| 33 |
|
causs |
|- ( ( D e. ( *Met ` X ) /\ F : NN --> Y ) -> ( F e. ( Cau ` D ) <-> F e. ( Cau ` ( D |` ( Y X. Y ) ) ) ) ) |
| 34 |
32 12 33
|
syl2anc |
|- ( ph -> ( F e. ( Cau ` D ) <-> F e. ( Cau ` ( D |` ( Y X. Y ) ) ) ) ) |
| 35 |
28 34
|
mpbid |
|- ( ph -> F e. ( Cau ` ( D |` ( Y X. Y ) ) ) ) |
| 36 |
|
eqid |
|- ( MetOpen ` ( D |` ( Y X. Y ) ) ) = ( MetOpen ` ( D |` ( Y X. Y ) ) ) |
| 37 |
36
|
cmetcau |
|- ( ( ( D |` ( Y X. Y ) ) e. ( CMet ` ( BaseSet ` W ) ) /\ F e. ( Cau ` ( D |` ( Y X. Y ) ) ) ) -> F e. dom ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ) |
| 38 |
27 35 37
|
syl2anc |
|- ( ph -> F e. dom ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ) |
| 39 |
|
xmetres |
|- ( D e. ( *Met ` X ) -> ( D |` ( Y X. Y ) ) e. ( *Met ` ( X i^i Y ) ) ) |
| 40 |
36
|
methaus |
|- ( ( D |` ( Y X. Y ) ) e. ( *Met ` ( X i^i Y ) ) -> ( MetOpen ` ( D |` ( Y X. Y ) ) ) e. Haus ) |
| 41 |
32 39 40
|
3syl |
|- ( ph -> ( MetOpen ` ( D |` ( Y X. Y ) ) ) e. Haus ) |
| 42 |
|
lmfun |
|- ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) e. Haus -> Fun ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ) |
| 43 |
|
funfvbrb |
|- ( Fun ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) -> ( F e. dom ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) <-> F ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) ) ) |
| 44 |
41 42 43
|
3syl |
|- ( ph -> ( F e. dom ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) <-> F ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) ) ) |
| 45 |
38 44
|
mpbid |
|- ( ph -> F ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) ) |