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 syl5bb
 |-  ( ( 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 ) ) )