MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  minveclem3OLD Structured version   Visualization version   Unicode version

Theorem minveclem3OLD 22438
Description: Lemma for minvecOLD 22445. The filter formed by taking elements successively closer to the infimum is Cauchy. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) Obsolete version of minveclem3 22426 as of 3-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
minvecOLD.x  |-  X  =  ( Base `  U
)
minvecOLD.m  |-  .-  =  ( -g `  U )
minvecOLD.n  |-  N  =  ( norm `  U
)
minvecOLD.u  |-  ( ph  ->  U  e.  CPreHil )
minvecOLD.y  |-  ( ph  ->  Y  e.  ( LSubSp `  U ) )
minvecOLD.w  |-  ( ph  ->  ( Us  Y )  e. CMetSp )
minvecOLD.a  |-  ( ph  ->  A  e.  X )
minvecOLD.j  |-  J  =  ( TopOpen `  U )
minvecOLD.r  |-  R  =  ran  ( y  e.  Y  |->  ( N `  ( A  .-  y ) ) )
minvecOLD.s  |-  S  =  sup ( R ,  RR ,  `'  <  )
minvecOLD.d  |-  D  =  ( ( dist `  U
)  |`  ( X  X.  X ) )
minvecOLD.f  |-  F  =  ran  ( r  e.  RR+  |->  { y  e.  Y  |  ( ( A D y ) ^ 2 )  <_ 
( ( S ^
2 )  +  r ) } )
Assertion
Ref Expression
minveclem3OLD  |-  ( ph  ->  ( Y filGen F )  e.  (CauFil `  ( D  |`  ( Y  X.  Y ) ) ) )
Distinct variable groups:    y,  .-    y, r, A    J, r,
y    y, F    y, N    ph, r, y    y, R   
y, U    X, r,
y    Y, r, y    D, r, y    S, r, y
Allowed substitution hints:    R( r)    U( r)    F( r)    .- ( r)    N( r)

Proof of Theorem minveclem3OLD
Dummy variables  w  s  u  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 467 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  RR+ )  ->  s  e.  RR+ )
2 2z 11003 . . . . . . . . 9  |-  2  e.  ZZ
3 rpexpcl 12329 . . . . . . . . 9  |-  ( ( s  e.  RR+  /\  2  e.  ZZ )  ->  (
s ^ 2 )  e.  RR+ )
41, 2, 3sylancl 673 . . . . . . . 8  |-  ( (
ph  /\  s  e.  RR+ )  ->  ( s ^ 2 )  e.  RR+ )
54rphalfcld 11387 . . . . . . 7  |-  ( (
ph  /\  s  e.  RR+ )  ->  ( (
s ^ 2 )  /  2 )  e.  RR+ )
6 4nn 10803 . . . . . . . 8  |-  4  e.  NN
7 nnrp 11345 . . . . . . . 8  |-  ( 4  e.  NN  ->  4  e.  RR+ )
86, 7ax-mp 5 . . . . . . 7  |-  4  e.  RR+
9 rpdivcl 11359 . . . . . . 7  |-  ( ( ( ( s ^
2 )  /  2
)  e.  RR+  /\  4  e.  RR+ )  ->  (
( ( s ^
2 )  /  2
)  /  4 )  e.  RR+ )
105, 8, 9sylancl 673 . . . . . 6  |-  ( (
ph  /\  s  e.  RR+ )  ->  ( (
( s ^ 2 )  /  2 )  /  4 )  e.  RR+ )
11 minvecOLD.y . . . . . . . 8  |-  ( ph  ->  Y  e.  ( LSubSp `  U ) )
1211adantr 471 . . . . . . 7  |-  ( (
ph  /\  s  e.  RR+ )  ->  Y  e.  ( LSubSp `  U )
)
13 rabexg 4570 . . . . . . 7  |-  ( Y  e.  ( LSubSp `  U
)  ->  { y  e.  Y  |  (
( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) }  e.  _V )
1412, 13syl 17 . . . . . 6  |-  ( (
ph  /\  s  e.  RR+ )  ->  { y  e.  Y  |  (
( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) }  e.  _V )
15 eqid 2462 . . . . . . 7  |-  ( r  e.  RR+  |->  { y  e.  Y  |  ( ( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  r ) } )  =  ( r  e.  RR+  |->  { y  e.  Y  |  ( ( A D y ) ^ 2 )  <_ 
( ( S ^
2 )  +  r ) } )
16 oveq2 6328 . . . . . . . . 9  |-  ( r  =  ( ( ( s ^ 2 )  /  2 )  / 
4 )  ->  (
( S ^ 2 )  +  r )  =  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )
1716breq2d 4430 . . . . . . . 8  |-  ( r  =  ( ( ( s ^ 2 )  /  2 )  / 
4 )  ->  (
( ( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  r )  <->  ( ( A D y ) ^
2 )  <_  (
( S ^ 2 )  +  ( ( ( s ^ 2 )  /  2 )  /  4 ) ) ) )
1817rabbidv 3048 . . . . . . 7  |-  ( r  =  ( ( ( s ^ 2 )  /  2 )  / 
4 )  ->  { y  e.  Y  |  ( ( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  r ) }  =  { y  e.  Y  |  ( ( A D y ) ^
2 )  <_  (
( S ^ 2 )  +  ( ( ( s ^ 2 )  /  2 )  /  4 ) ) } )
1915, 18elrnmpt1s 5104 . . . . . 6  |-  ( ( ( ( ( s ^ 2 )  / 
2 )  /  4
)  e.  RR+  /\  {
y  e.  Y  | 
( ( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) }  e.  _V )  ->  { y  e.  Y  |  ( ( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) }  e.  ran  ( r  e.  RR+  |->  { y  e.  Y  |  ( ( A D y ) ^
2 )  <_  (
( S ^ 2 )  +  r ) } ) )
2010, 14, 19syl2anc 671 . . . . 5  |-  ( (
ph  /\  s  e.  RR+ )  ->  { y  e.  Y  |  (
( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) }  e.  ran  ( r  e.  RR+  |->  { y  e.  Y  |  ( ( A D y ) ^
2 )  <_  (
( S ^ 2 )  +  r ) } ) )
21 minvecOLD.f . . . . 5  |-  F  =  ran  ( r  e.  RR+  |->  { y  e.  Y  |  ( ( A D y ) ^ 2 )  <_ 
( ( S ^
2 )  +  r ) } )
2220, 21syl6eleqr 2551 . . . 4  |-  ( (
ph  /\  s  e.  RR+ )  ->  { y  e.  Y  |  (
( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) }  e.  F )
23 oveq2 6328 . . . . . . . . . 10  |-  ( y  =  u  ->  ( A D y )  =  ( A D u ) )
2423oveq1d 6335 . . . . . . . . 9  |-  ( y  =  u  ->  (
( A D y ) ^ 2 )  =  ( ( A D u ) ^
2 ) )
2524breq1d 4428 . . . . . . . 8  |-  ( y  =  u  ->  (
( ( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) )  <->  ( ( A D u ) ^
2 )  <_  (
( S ^ 2 )  +  ( ( ( s ^ 2 )  /  2 )  /  4 ) ) ) )
2625elrab 3208 . . . . . . 7  |-  ( u  e.  { y  e.  Y  |  ( ( A D y ) ^ 2 )  <_ 
( ( S ^
2 )  +  ( ( ( s ^
2 )  /  2
)  /  4 ) ) }  <->  ( u  e.  Y  /\  (
( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) )
27 oveq2 6328 . . . . . . . . . 10  |-  ( y  =  v  ->  ( A D y )  =  ( A D v ) )
2827oveq1d 6335 . . . . . . . . 9  |-  ( y  =  v  ->  (
( A D y ) ^ 2 )  =  ( ( A D v ) ^
2 ) )
2928breq1d 4428 . . . . . . . 8  |-  ( y  =  v  ->  (
( ( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) )  <->  ( ( A D v ) ^
2 )  <_  (
( S ^ 2 )  +  ( ( ( s ^ 2 )  /  2 )  /  4 ) ) ) )
3029elrab 3208 . . . . . . 7  |-  ( v  e.  { y  e.  Y  |  ( ( A D y ) ^ 2 )  <_ 
( ( S ^
2 )  +  ( ( ( s ^
2 )  /  2
)  /  4 ) ) }  <->  ( v  e.  Y  /\  (
( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) )
3126, 30anbi12i 708 . . . . . 6  |-  ( ( u  e.  { y  e.  Y  |  ( ( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) }  /\  v  e.  { y  e.  Y  |  (
( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) } )  <-> 
( ( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_ 
( ( S ^
2 )  +  ( ( ( s ^
2 )  /  2
)  /  4 ) ) )  /\  (
v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )
32 simprll 777 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  u  e.  Y )
33 simprrl 779 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  v  e.  Y )
3432, 33ovresd 6469 . . . . . . 7  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( u
( D  |`  ( Y  X.  Y ) ) v )  =  ( u D v ) )
35 minvecOLD.u . . . . . . . . . . . . 13  |-  ( ph  ->  U  e.  CPreHil )
36 cphngp 22206 . . . . . . . . . . . . 13  |-  ( U  e.  CPreHil  ->  U  e. NrmGrp )
37 ngpms 21669 . . . . . . . . . . . . 13  |-  ( U  e. NrmGrp  ->  U  e.  MetSp )
38 minvecOLD.x . . . . . . . . . . . . . 14  |-  X  =  ( Base `  U
)
39 minvecOLD.d . . . . . . . . . . . . . 14  |-  D  =  ( ( dist `  U
)  |`  ( X  X.  X ) )
4038, 39msmet 21527 . . . . . . . . . . . . 13  |-  ( U  e.  MetSp  ->  D  e.  ( Met `  X ) )
4135, 36, 37, 404syl 19 . . . . . . . . . . . 12  |-  ( ph  ->  D  e.  ( Met `  X ) )
4241ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  D  e.  ( Met `  X ) )
43 eqid 2462 . . . . . . . . . . . . . . 15  |-  ( LSubSp `  U )  =  (
LSubSp `  U )
4438, 43lssss 18215 . . . . . . . . . . . . . 14  |-  ( Y  e.  ( LSubSp `  U
)  ->  Y  C_  X
)
4511, 44syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  C_  X )
4645ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  Y  C_  X
)
4746, 32sseldd 3445 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  u  e.  X )
4846, 33sseldd 3445 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  v  e.  X )
49 metcl 21402 . . . . . . . . . . 11  |-  ( ( D  e.  ( Met `  X )  /\  u  e.  X  /\  v  e.  X )  ->  (
u D v )  e.  RR )
5042, 47, 48, 49syl3anc 1276 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( u D v )  e.  RR )
5150resqcld 12480 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( (
u D v ) ^ 2 )  e.  RR )
525adantr 471 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( (
s ^ 2 )  /  2 )  e.  RR+ )
5352rpred 11375 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( (
s ^ 2 )  /  2 )  e.  RR )
544adantr 471 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( s ^ 2 )  e.  RR+ )
5554rpred 11375 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( s ^ 2 )  e.  RR )
56 minvecOLD.m . . . . . . . . . . 11  |-  .-  =  ( -g `  U )
57 minvecOLD.n . . . . . . . . . . 11  |-  N  =  ( norm `  U
)
5835ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  U  e.  CPreHil )
5911ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  Y  e.  ( LSubSp `  U )
)
60 minvecOLD.w . . . . . . . . . . . 12  |-  ( ph  ->  ( Us  Y )  e. CMetSp )
6160ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( Us  Y
)  e. CMetSp )
62 minvecOLD.a . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  X )
6362ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  A  e.  X )
64 minvecOLD.j . . . . . . . . . . 11  |-  J  =  ( TopOpen `  U )
65 minvecOLD.r . . . . . . . . . . 11  |-  R  =  ran  ( y  e.  Y  |->  ( N `  ( A  .-  y ) ) )
66 minvecOLD.s . . . . . . . . . . 11  |-  S  =  sup ( R ,  RR ,  `'  <  )
6710adantr 471 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( (
( s ^ 2 )  /  2 )  /  4 )  e.  RR+ )
6867rpred 11375 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( (
( s ^ 2 )  /  2 )  /  4 )  e.  RR )
6967rpge0d 11379 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  0  <_  ( ( ( s ^
2 )  /  2
)  /  4 ) )
70 simprlr 778 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( ( A D u ) ^
2 )  <_  (
( S ^ 2 )  +  ( ( ( s ^ 2 )  /  2 )  /  4 ) ) )
71 simprrr 780 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( ( A D v ) ^
2 )  <_  (
( S ^ 2 )  +  ( ( ( s ^ 2 )  /  2 )  /  4 ) ) )
7238, 56, 57, 58, 59, 61, 63, 64, 65, 66, 39, 68, 69, 32, 33, 70, 71minveclem2OLD 22435 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( (
u D v ) ^ 2 )  <_ 
( 4  x.  (
( ( s ^
2 )  /  2
)  /  4 ) ) )
7352rpcnd 11377 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( (
s ^ 2 )  /  2 )  e.  CC )
74 4cn 10720 . . . . . . . . . . . 12  |-  4  e.  CC
7574a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  4  e.  CC )
76 4ne0 10739 . . . . . . . . . . . 12  |-  4  =/=  0
7776a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  4  =/=  0 )
7873, 75, 77divcan2d 10418 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( 4  x.  ( ( ( s ^ 2 )  /  2 )  / 
4 ) )  =  ( ( s ^
2 )  /  2
) )
7972, 78breqtrd 4443 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( (
u D v ) ^ 2 )  <_ 
( ( s ^
2 )  /  2
) )
80 rphalflt 11363 . . . . . . . . . 10  |-  ( ( s ^ 2 )  e.  RR+  ->  ( ( s ^ 2 )  /  2 )  < 
( s ^ 2 ) )
8154, 80syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( (
s ^ 2 )  /  2 )  < 
( s ^ 2 ) )
8251, 53, 55, 79, 81lelttrd 9824 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( (
u D v ) ^ 2 )  < 
( s ^ 2 ) )
83 rpre 11342 . . . . . . . . . 10  |-  ( s  e.  RR+  ->  s  e.  RR )
8483ad2antlr 738 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  s  e.  RR )
85 metge0 21415 . . . . . . . . . 10  |-  ( ( D  e.  ( Met `  X )  /\  u  e.  X  /\  v  e.  X )  ->  0  <_  ( u D v ) )
8642, 47, 48, 85syl3anc 1276 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  0  <_  ( u D v ) )
87 rpge0 11348 . . . . . . . . . 10  |-  ( s  e.  RR+  ->  0  <_ 
s )
8887ad2antlr 738 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  0  <_  s )
8950, 84, 86, 88lt2sqd 12488 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( (
u D v )  <  s  <->  ( (
u D v ) ^ 2 )  < 
( s ^ 2 ) ) )
9082, 89mpbird 240 . . . . . . 7  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( u D v )  < 
s )
9134, 90eqbrtrd 4439 . . . . . 6  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
( u  e.  Y  /\  ( ( A D u ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) )  /\  ( v  e.  Y  /\  ( ( A D v ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) ) ) )  ->  ( u
( D  |`  ( Y  X.  Y ) ) v )  <  s
)
9231, 91sylan2b 482 . . . . 5  |-  ( ( ( ph  /\  s  e.  RR+ )  /\  (
u  e.  { y  e.  Y  |  ( ( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) }  /\  v  e.  { y  e.  Y  |  (
( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) } ) )  ->  ( u
( D  |`  ( Y  X.  Y ) ) v )  <  s
)
9392ralrimivva 2821 . . . 4  |-  ( (
ph  /\  s  e.  RR+ )  ->  A. u  e.  { y  e.  Y  |  ( ( A D y ) ^
2 )  <_  (
( S ^ 2 )  +  ( ( ( s ^ 2 )  /  2 )  /  4 ) ) } A. v  e. 
{ y  e.  Y  |  ( ( A D y ) ^
2 )  <_  (
( S ^ 2 )  +  ( ( ( s ^ 2 )  /  2 )  /  4 ) ) }  ( u ( D  |`  ( Y  X.  Y ) ) v )  <  s )
94 raleq 2999 . . . . . 6  |-  ( w  =  { y  e.  Y  |  ( ( A D y ) ^ 2 )  <_ 
( ( S ^
2 )  +  ( ( ( s ^
2 )  /  2
)  /  4 ) ) }  ->  ( A. v  e.  w  ( u ( D  |`  ( Y  X.  Y
) ) v )  <  s  <->  A. v  e.  { y  e.  Y  |  ( ( A D y ) ^
2 )  <_  (
( S ^ 2 )  +  ( ( ( s ^ 2 )  /  2 )  /  4 ) ) }  ( u ( D  |`  ( Y  X.  Y ) ) v )  <  s ) )
9594raleqbi1dv 3007 . . . . 5  |-  ( w  =  { y  e.  Y  |  ( ( A D y ) ^ 2 )  <_ 
( ( S ^
2 )  +  ( ( ( s ^
2 )  /  2
)  /  4 ) ) }  ->  ( A. u  e.  w  A. v  e.  w  ( u ( D  |`  ( Y  X.  Y
) ) v )  <  s  <->  A. u  e.  { y  e.  Y  |  ( ( A D y ) ^
2 )  <_  (
( S ^ 2 )  +  ( ( ( s ^ 2 )  /  2 )  /  4 ) ) } A. v  e. 
{ y  e.  Y  |  ( ( A D y ) ^
2 )  <_  (
( S ^ 2 )  +  ( ( ( s ^ 2 )  /  2 )  /  4 ) ) }  ( u ( D  |`  ( Y  X.  Y ) ) v )  <  s ) )
9695rspcev 3162 . . . 4  |-  ( ( { y  e.  Y  |  ( ( A D y ) ^
2 )  <_  (
( S ^ 2 )  +  ( ( ( s ^ 2 )  /  2 )  /  4 ) ) }  e.  F  /\  A. u  e.  { y  e.  Y  |  ( ( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) } A. v  e.  { y  e.  Y  |  (
( A D y ) ^ 2 )  <_  ( ( S ^ 2 )  +  ( ( ( s ^ 2 )  / 
2 )  /  4
) ) }  (
u ( D  |`  ( Y  X.  Y
) ) v )  <  s )  ->  E. w  e.  F  A. u  e.  w  A. v  e.  w  ( u ( D  |`  ( Y  X.  Y
) ) v )  <  s )
9722, 93, 96syl2anc 671 . . 3  |-  ( (
ph  /\  s  e.  RR+ )  ->  E. w  e.  F  A. u  e.  w  A. v  e.  w  ( u
( D  |`  ( Y  X.  Y ) ) v )  <  s
)
9897ralrimiva 2814 . 2  |-  ( ph  ->  A. s  e.  RR+  E. w  e.  F  A. u  e.  w  A. v  e.  w  (
u ( D  |`  ( Y  X.  Y
) ) v )  <  s )
9938, 56, 57, 35, 11, 60, 62, 64, 65, 66, 39minveclem3aOLD 22436 . . . 4  |-  ( ph  ->  ( D  |`  ( Y  X.  Y ) )  e.  ( CMet `  Y
) )
100 cmetmet 22311 . . . 4  |-  ( ( D  |`  ( Y  X.  Y ) )  e.  ( CMet `  Y
)  ->  ( D  |`  ( Y  X.  Y
) )  e.  ( Met `  Y ) )
101 metxmet 21404 . . . 4  |-  ( ( D  |`  ( Y  X.  Y ) )  e.  ( Met `  Y
)  ->  ( D  |`  ( Y  X.  Y
) )  e.  ( *Met `  Y
) )
10299, 100, 1013syl 18 . . 3  |-  ( ph  ->  ( D  |`  ( Y  X.  Y ) )  e.  ( *Met `  Y ) )
10338, 56, 57, 35, 11, 60, 62, 64, 65, 66, 39, 21minveclem3bOLD 22437 . . 3  |-  ( ph  ->  F  e.  ( fBas `  Y ) )
104 fgcfil 22296 . . 3  |-  ( ( ( D  |`  ( Y  X.  Y ) )  e.  ( *Met `  Y )  /\  F  e.  ( fBas `  Y
) )  ->  (
( Y filGen F )  e.  (CauFil `  ( D  |`  ( Y  X.  Y ) ) )  <->  A. s  e.  RR+  E. w  e.  F  A. u  e.  w  A. v  e.  w  ( u
( D  |`  ( Y  X.  Y ) ) v )  <  s
) )
105102, 103, 104syl2anc 671 . 2  |-  ( ph  ->  ( ( Y filGen F )  e.  (CauFil `  ( D  |`  ( Y  X.  Y ) ) )  <->  A. s  e.  RR+  E. w  e.  F  A. u  e.  w  A. v  e.  w  (
u ( D  |`  ( Y  X.  Y
) ) v )  <  s ) )
10698, 105mpbird 240 1  |-  ( ph  ->  ( Y filGen F )  e.  (CauFil `  ( D  |`  ( Y  X.  Y ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1455    e. wcel 1898    =/= wne 2633   A.wral 2749   E.wrex 2750   {crab 2753   _Vcvv 3057    C_ wss 3416   class class class wbr 4418    |-> cmpt 4477    X. cxp 4854   `'ccnv 4855   ran crn 4857    |` cres 4858   ` cfv 5605  (class class class)co 6320   supcsup 7985   CCcc 9568   RRcr 9569   0cc0 9570    + caddc 9573    x. cmul 9575    < clt 9706    <_ cle 9707    / cdiv 10302   NNcn 10642   2c2 10692   4c4 10694   ZZcz 10971   RR+crp 11336   ^cexp 12310   Basecbs 15176   ↾s cress 15177   distcds 15254   TopOpenctopn 15375   -gcsg 16726   LSubSpclss 18210   *Metcxmt 19010   Metcme 19011   fBascfbas 19013   filGencfg 19014   MetSpcmt 21388   normcnm 21646  NrmGrpcngp 21647   CPreHilccph 22199  CauFilccfil 22277   CMetcms 22279  CMetSpccms 22355
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-inf2 8177  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647  ax-pre-sup 9648  ax-addf 9649  ax-mulf 9650
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-isom 5614  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-1st 6825  df-2nd 6826  df-tpos 7004  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-1o 7213  df-oadd 7217  df-er 7394  df-map 7505  df-en 7601  df-dom 7602  df-sdom 7603  df-fin 7604  df-sup 7987  df-inf 7988  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-div 10303  df-nn 10643  df-2 10701  df-3 10702  df-4 10703  df-5 10704  df-6 10705  df-7 10706  df-8 10707  df-9 10708  df-10 10709  df-n0 10904  df-z 10972  df-dec 11086  df-uz 11194  df-q 11299  df-rp 11337  df-xneg 11443  df-xadd 11444  df-xmul 11445  df-ico 11675  df-fz 11820  df-seq 12252  df-exp 12311  df-cj 13217  df-re 13218  df-im 13219  df-sqrt 13353  df-abs 13354  df-struct 15178  df-ndx 15179  df-slot 15180  df-base 15181  df-sets 15182  df-ress 15183  df-plusg 15258  df-mulr 15259  df-starv 15260  df-sca 15261  df-vsca 15262  df-ip 15263  df-tset 15264  df-ple 15265  df-ds 15267  df-unif 15268  df-0g 15395  df-topgen 15397  df-mgm 16543  df-sgrp 16582  df-mnd 16592  df-mhm 16637  df-grp 16728  df-minusg 16729  df-sbg 16730  df-mulg 16731  df-subg 16869  df-ghm 16936  df-cmn 17487  df-abl 17488  df-mgp 17779  df-ur 17791  df-ring 17837  df-cring 17838  df-oppr 17906  df-dvdsr 17924  df-unit 17925  df-invr 17955  df-dvr 17966  df-rnghom 17998  df-drng 18032  df-subrg 18061  df-staf 18128  df-srng 18129  df-lmod 18148  df-lss 18211  df-lmhm 18300  df-lvec 18381  df-sra 18450  df-rgmod 18451  df-psmet 19017  df-xmet 19018  df-met 19019  df-bl 19020  df-mopn 19021  df-fbas 19022  df-fg 19023  df-cnfld 19026  df-phl 19248  df-top 19976  df-bases 19977  df-topon 19978  df-topsp 19979  df-fil 20916  df-xms 21390  df-ms 21391  df-nm 21652  df-ngp 21653  df-nlm 21656  df-clm 22149  df-cph 22201  df-cfil 22280  df-cmet 22282  df-cms 22358
This theorem is referenced by:  minveclem4aOLD  22439
  Copyright terms: Public domain W3C validator