Metamath Proof Explorer

Theorem minvecolem7

Description: Lemma for minveco . Since any two minimal points are distance zero away from each other, the minimal point is unique. (Contributed by Mario Carneiro, 9-May-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 , < )
Assertion minvecolem7 
|- ( ph -> E! x e. Y 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 1 2 3 4 5 6 7 8 9 10 11 minvecolem5 
 |-  ( ph -> E. x e. Y A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) )
13 5 ad2antrr 
 |-  ( ( ( ph /\ ( x e. Y /\ w e. Y ) ) /\ ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) ) -> U e. CPreHilOLD )
14 6 ad2antrr 
 |-  ( ( ( ph /\ ( x e. Y /\ w e. Y ) ) /\ ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) ) -> W e. ( ( SubSp ` U ) i^i CBan ) )
15 7 ad2antrr 
 |-  ( ( ( ph /\ ( x e. Y /\ w e. Y ) ) /\ ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) ) -> A e. X )
16 0re 
 |-  0 e. RR
17 16 a1i 
 |-  ( ( ( ph /\ ( x e. Y /\ w e. Y ) ) /\ ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) ) -> 0 e. RR )
18 0le0 
 |-  0 <_ 0
19 18 a1i 
 |-  ( ( ( ph /\ ( x e. Y /\ w e. Y ) ) /\ ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) ) -> 0 <_ 0 )
20 simplrl 
 |-  ( ( ( ph /\ ( x e. Y /\ w e. Y ) ) /\ ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) ) -> x e. Y )
21 simplrr 
 |-  ( ( ( ph /\ ( x e. Y /\ w e. Y ) ) /\ ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) ) -> w e. Y )
22 simprl 
 |-  ( ( ( ph /\ ( x e. Y /\ w e. Y ) ) /\ ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) ) -> ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) )
23 simprr 
 |-  ( ( ( ph /\ ( x e. Y /\ w e. Y ) ) /\ ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) ) -> ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) )
24 1 2 3 4 13 14 15 8 9 10 11 17 19 20 21 22 23 minvecolem2 
 |-  ( ( ( ph /\ ( x e. Y /\ w e. Y ) ) /\ ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) ) -> ( ( x D w ) ^ 2 ) <_ ( 4 x. 0 ) )
25 24 ex 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) -> ( ( x D w ) ^ 2 ) <_ ( 4 x. 0 ) ) )
26 1 2 3 4 5 6 7 8 9 10 11 minvecolem6 
 |-  ( ( ph /\ x e. Y ) -> ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) ) )
27 26 adantrr 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) ) )
28 1 2 3 4 5 6 7 8 9 10 11 minvecolem6 
 |-  ( ( ph /\ w e. Y ) -> ( ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. y e. Y ( N ` ( A M w ) ) <_ ( N ` ( A M y ) ) ) )
29 28 adantrl 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. y e. Y ( N ` ( A M w ) ) <_ ( N ` ( A M y ) ) ) )
30 27 29 anbi12d 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) <-> ( A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) /\ A. y e. Y ( N ` ( A M w ) ) <_ ( N ` ( A M y ) ) ) ) )
31 4cn 
 |-  4 e. CC
32 31 mul01i 
 |-  ( 4 x. 0 ) = 0
33 32 breq2i 
 |-  ( ( ( x D w ) ^ 2 ) <_ ( 4 x. 0 ) <-> ( ( x D w ) ^ 2 ) <_ 0 )
34 phnv 
 |-  ( U e. CPreHilOLD -> U e. NrmCVec )
35 5 34 syl 
 |-  ( ph -> U e. NrmCVec )
36 35 adantr 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> U e. NrmCVec )
37 1 8 imsmet 
 |-  ( U e. NrmCVec -> D e. ( Met ` X ) )
38 36 37 syl 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> D e. ( Met ` X ) )
39 inss1 
 |-  ( ( SubSp ` U ) i^i CBan ) C_ ( SubSp ` U )
40 39 6 sselid 
 |-  ( ph -> W e. ( SubSp ` U ) )
41 eqid 
 |-  ( SubSp ` U ) = ( SubSp ` U )
42 1 4 41 sspba 
 |-  ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) -> Y C_ X )
43 35 40 42 syl2anc 
 |-  ( ph -> Y C_ X )
44 43 adantr 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> Y C_ X )
45 simprl 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> x e. Y )
46 44 45 sseldd 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> x e. X )
47 simprr 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> w e. Y )
48 44 47 sseldd 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> w e. X )
49 metcl 
 |-  ( ( D e. ( Met ` X ) /\ x e. X /\ w e. X ) -> ( x D w ) e. RR )
50 38 46 48 49 syl3anc 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( x D w ) e. RR )
51 50 sqge0d 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> 0 <_ ( ( x D w ) ^ 2 ) )
52 51 biantrud 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( ( x D w ) ^ 2 ) <_ 0 <-> ( ( ( x D w ) ^ 2 ) <_ 0 /\ 0 <_ ( ( x D w ) ^ 2 ) ) ) )
53 50 resqcld 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( x D w ) ^ 2 ) e. RR )
54 letri3 
 |-  ( ( ( ( x D w ) ^ 2 ) e. RR /\ 0 e. RR ) -> ( ( ( x D w ) ^ 2 ) = 0 <-> ( ( ( x D w ) ^ 2 ) <_ 0 /\ 0 <_ ( ( x D w ) ^ 2 ) ) ) )
55 53 16 54 sylancl 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( ( x D w ) ^ 2 ) = 0 <-> ( ( ( x D w ) ^ 2 ) <_ 0 /\ 0 <_ ( ( x D w ) ^ 2 ) ) ) )
56 50 recnd 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( x D w ) e. CC )
57 sqeq0 
 |-  ( ( x D w ) e. CC -> ( ( ( x D w ) ^ 2 ) = 0 <-> ( x D w ) = 0 ) )
58 56 57 syl 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( ( x D w ) ^ 2 ) = 0 <-> ( x D w ) = 0 ) )
59 meteq0 
 |-  ( ( D e. ( Met ` X ) /\ x e. X /\ w e. X ) -> ( ( x D w ) = 0 <-> x = w ) )
60 38 46 48 59 syl3anc 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( x D w ) = 0 <-> x = w ) )
61 58 60 bitrd 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( ( x D w ) ^ 2 ) = 0 <-> x = w ) )
62 52 55 61 3bitr2d 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( ( x D w ) ^ 2 ) <_ 0 <-> x = w ) )
63 33 62 bitrid 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( ( x D w ) ^ 2 ) <_ ( 4 x. 0 ) <-> x = w ) )
64 25 30 63 3imtr3d 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) /\ A. y e. Y ( N ` ( A M w ) ) <_ ( N ` ( A M y ) ) ) -> x = w ) )
65 64 ralrimivva 
 |-  ( ph -> A. x e. Y A. w e. Y ( ( A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) /\ A. y e. Y ( N ` ( A M w ) ) <_ ( N ` ( A M y ) ) ) -> x = w ) )
66 oveq2 
 |-  ( x = w -> ( A M x ) = ( A M w ) )
67 66 fveq2d 
 |-  ( x = w -> ( N ` ( A M x ) ) = ( N ` ( A M w ) ) )
68 67 breq1d 
 |-  ( x = w -> ( ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) <-> ( N ` ( A M w ) ) <_ ( N ` ( A M y ) ) ) )
69 68 ralbidv 
 |-  ( x = w -> ( A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) <-> A. y e. Y ( N ` ( A M w ) ) <_ ( N ` ( A M y ) ) ) )
70 69 reu4 
 |-  ( E! x e. Y A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) <-> ( E. x e. Y A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) /\ A. x e. Y A. w e. Y ( ( A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) /\ A. y e. Y ( N ` ( A M w ) ) <_ ( N ` ( A M y ) ) ) -> x = w ) ) )
71 12 65 70 sylanbrc 
 |-  ( ph -> E! x e. Y A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) )