Metamath Proof Explorer

Theorem minvecolem6

Description: Lemma for minveco . Any minimal point is less than S away from A . (Contributed by Mario Carneiro, 9-May-2014) (Revised by AV, 4-Oct-2020) (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 , < )
Assertion minvecolem6 
|- ( ( ph /\ x e. Y ) -> ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) ) )

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 phnv 
 |-  ( U e. CPreHilOLD -> U e. NrmCVec )
13 5 12 syl 
 |-  ( ph -> U e. NrmCVec )
14 13 adantr 
 |-  ( ( ph /\ x e. Y ) -> U e. NrmCVec )
15 7 adantr 
 |-  ( ( ph /\ x e. Y ) -> A e. X )
16 inss1 
 |-  ( ( SubSp ` U ) i^i CBan ) C_ ( SubSp ` U )
17 16 6 sselid 
 |-  ( ph -> W e. ( SubSp ` U ) )
18 eqid 
 |-  ( SubSp ` U ) = ( SubSp ` U )
19 1 4 18 sspba 
 |-  ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) -> Y C_ X )
20 13 17 19 syl2anc 
 |-  ( ph -> Y C_ X )
21 20 sselda 
 |-  ( ( ph /\ x e. Y ) -> x e. X )
22 1 2 3 8 imsdval 
 |-  ( ( U e. NrmCVec /\ A e. X /\ x e. X ) -> ( A D x ) = ( N ` ( A M x ) ) )
23 14 15 21 22 syl3anc 
 |-  ( ( ph /\ x e. Y ) -> ( A D x ) = ( N ` ( A M x ) ) )
24 23 oveq1d 
 |-  ( ( ph /\ x e. Y ) -> ( ( A D x ) ^ 2 ) = ( ( N ` ( A M x ) ) ^ 2 ) )
25 1 2 3 4 5 6 7 8 9 10 minvecolem1 
 |-  ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )
26 25 adantr 
 |-  ( ( ph /\ x e. Y ) -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )
27 26 simp1d 
 |-  ( ( ph /\ x e. Y ) -> R C_ RR )
28 26 simp2d 
 |-  ( ( ph /\ x e. Y ) -> R =/= (/) )
29 0red 
 |-  ( ( ph /\ x e. Y ) -> 0 e. RR )
30 26 simp3d 
 |-  ( ( ph /\ x e. Y ) -> A. w e. R 0 <_ w )
31 breq1 
 |-  ( x = 0 -> ( x <_ w <-> 0 <_ w ) )
32 31 ralbidv 
 |-  ( x = 0 -> ( A. w e. R x <_ w <-> A. w e. R 0 <_ w ) )
33 32 rspcev 
 |-  ( ( 0 e. RR /\ A. w e. R 0 <_ w ) -> E. x e. RR A. w e. R x <_ w )
34 29 30 33 syl2anc 
 |-  ( ( ph /\ x e. Y ) -> E. x e. RR A. w e. R x <_ w )
35 infrecl 
 |-  ( ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) -> inf ( R , RR , < ) e. RR )
36 27 28 34 35 syl3anc 
 |-  ( ( ph /\ x e. Y ) -> inf ( R , RR , < ) e. RR )
37 11 36 eqeltrid 
 |-  ( ( ph /\ x e. Y ) -> S e. RR )
38 37 resqcld 
 |-  ( ( ph /\ x e. Y ) -> ( S ^ 2 ) e. RR )
39 38 recnd 
 |-  ( ( ph /\ x e. Y ) -> ( S ^ 2 ) e. CC )
40 39 addridd 
 |-  ( ( ph /\ x e. Y ) -> ( ( S ^ 2 ) + 0 ) = ( S ^ 2 ) )
41 24 40 breq12d 
 |-  ( ( ph /\ x e. Y ) -> ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> ( ( N ` ( A M x ) ) ^ 2 ) <_ ( S ^ 2 ) ) )
42 1 2 nvmcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ x e. X ) -> ( A M x ) e. X )
43 14 15 21 42 syl3anc 
 |-  ( ( ph /\ x e. Y ) -> ( A M x ) e. X )
44 1 3 nvcl 
 |-  ( ( U e. NrmCVec /\ ( A M x ) e. X ) -> ( N ` ( A M x ) ) e. RR )
45 14 43 44 syl2anc 
 |-  ( ( ph /\ x e. Y ) -> ( N ` ( A M x ) ) e. RR )
46 1 3 nvge0 
 |-  ( ( U e. NrmCVec /\ ( A M x ) e. X ) -> 0 <_ ( N ` ( A M x ) ) )
47 14 43 46 syl2anc 
 |-  ( ( ph /\ x e. Y ) -> 0 <_ ( N ` ( A M x ) ) )
48 infregelb 
 |-  ( ( ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) /\ 0 e. RR ) -> ( 0 <_ inf ( R , RR , < ) <-> A. w e. R 0 <_ w ) )
49 27 28 34 29 48 syl31anc 
 |-  ( ( ph /\ x e. Y ) -> ( 0 <_ inf ( R , RR , < ) <-> A. w e. R 0 <_ w ) )
50 30 49 mpbird 
 |-  ( ( ph /\ x e. Y ) -> 0 <_ inf ( R , RR , < ) )
51 50 11 breqtrrdi 
 |-  ( ( ph /\ x e. Y ) -> 0 <_ S )
52 45 37 47 51 le2sqd 
 |-  ( ( ph /\ x e. Y ) -> ( ( N ` ( A M x ) ) <_ S <-> ( ( N ` ( A M x ) ) ^ 2 ) <_ ( S ^ 2 ) ) )
53 11 breq2i 
 |-  ( ( N ` ( A M x ) ) <_ S <-> ( N ` ( A M x ) ) <_ inf ( R , RR , < ) )
54 infregelb 
 |-  ( ( ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) /\ ( N ` ( A M x ) ) e. RR ) -> ( ( N ` ( A M x ) ) <_ inf ( R , RR , < ) <-> A. w e. R ( N ` ( A M x ) ) <_ w ) )
55 27 28 34 45 54 syl31anc 
 |-  ( ( ph /\ x e. Y ) -> ( ( N ` ( A M x ) ) <_ inf ( R , RR , < ) <-> A. w e. R ( N ` ( A M x ) ) <_ w ) )
56 53 55 bitrid 
 |-  ( ( ph /\ x e. Y ) -> ( ( N ` ( A M x ) ) <_ S <-> A. w e. R ( N ` ( A M x ) ) <_ w ) )
57 41 52 56 3bitr2d 
 |-  ( ( ph /\ x e. Y ) -> ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. w e. R ( N ` ( A M x ) ) <_ w ) )
58 10 raleqi 
 |-  ( A. w e. R ( N ` ( A M x ) ) <_ w <-> A. w e. ran ( y e. Y |-> ( N ` ( A M y ) ) ) ( N ` ( A M x ) ) <_ w )
59 fvex 
 |-  ( N ` ( A M y ) ) e. _V
60 59 rgenw 
 |-  A. y e. Y ( N ` ( A M y ) ) e. _V
61 eqid 
 |-  ( y e. Y |-> ( N ` ( A M y ) ) ) = ( y e. Y |-> ( N ` ( A M y ) ) )
62 breq2 
 |-  ( w = ( N ` ( A M y ) ) -> ( ( N ` ( A M x ) ) <_ w <-> ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) ) )
63 61 62 ralrnmptw 
 |-  ( A. y e. Y ( N ` ( A M y ) ) e. _V -> ( A. w e. ran ( y e. Y |-> ( N ` ( A M y ) ) ) ( N ` ( A M x ) ) <_ w <-> A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) ) )
64 60 63 ax-mp 
 |-  ( A. w e. ran ( y e. Y |-> ( N ` ( A M y ) ) ) ( N ` ( A M x ) ) <_ w <-> A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) )
65 58 64 bitri 
 |-  ( A. w e. R ( N ` ( A M x ) ) <_ w <-> A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) )
66 57 65 bitrdi 
 |-  ( ( ph /\ x e. Y ) -> ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) ) )