Metamath Proof Explorer

Theorem minveclem5

Description: Lemma for minvec . Discharge the assumptions in minveclem4 . (Contributed by Mario Carneiro, 9-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 ) )
Assertion minveclem5 
|- ( ph -> E. x e. Y A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- 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 oveq2 
 |-  ( s = r -> ( ( S ^ 2 ) + s ) = ( ( S ^ 2 ) + r ) )
13 12 breq2d 
 |-  ( s = r -> ( ( ( A D z ) ^ 2 ) <_ ( ( S ^ 2 ) + s ) <-> ( ( A D z ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) ) )
14 13 rabbidv 
 |-  ( s = r -> { z e. Y | ( ( A D z ) ^ 2 ) <_ ( ( S ^ 2 ) + s ) } = { z e. Y | ( ( A D z ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
15 oveq2 
 |-  ( z = y -> ( A D z ) = ( A D y ) )
16 15 oveq1d 
 |-  ( z = y -> ( ( A D z ) ^ 2 ) = ( ( A D y ) ^ 2 ) )
17 16 breq1d 
 |-  ( z = y -> ( ( ( A D z ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) <-> ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) ) )
18 17 cbvrabv 
 |-  { z e. Y | ( ( A D z ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } = { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) }
19 14 18 eqtrdi 
 |-  ( s = r -> { z e. Y | ( ( A D z ) ^ 2 ) <_ ( ( S ^ 2 ) + s ) } = { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
20 19 cbvmptv 
 |-  ( s e. RR+ |-> { z e. Y | ( ( A D z ) ^ 2 ) <_ ( ( S ^ 2 ) + s ) } ) = ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
21 20 rneqi 
 |-  ran ( s e. RR+ |-> { z e. Y | ( ( A D z ) ^ 2 ) <_ ( ( S ^ 2 ) + s ) } ) = ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
22 eqid 
 |-  U. ( J fLim ( X filGen ran ( s e. RR+ |-> { z e. Y | ( ( A D z ) ^ 2 ) <_ ( ( S ^ 2 ) + s ) } ) ) ) = U. ( J fLim ( X filGen ran ( s e. RR+ |-> { z e. Y | ( ( A D z ) ^ 2 ) <_ ( ( S ^ 2 ) + s ) } ) ) )
23 eqid 
 |-  ( ( ( ( ( A D U. ( J fLim ( X filGen ran ( s e. RR+ |-> { z e. Y | ( ( A D z ) ^ 2 ) <_ ( ( S ^ 2 ) + s ) } ) ) ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) = ( ( ( ( ( A D U. ( J fLim ( X filGen ran ( s e. RR+ |-> { z e. Y | ( ( A D z ) ^ 2 ) <_ ( ( S ^ 2 ) + s ) } ) ) ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) )
24 1 2 3 4 5 6 7 8 9 10 11 21 22 23 minveclem4 
 |-  ( ph -> E. x e. Y A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) )