Metamath Proof Explorer

Theorem minveclem7

Description: Lemma for minvec . Since any two minimal points are distance zero away from each other, the minimal point is unique. (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 minveclem7 
|- ( 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 1 2 3 4 5 6 7 8 9 10 11 minveclem5 
 |-  ( ph -> E. x e. Y A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) )
13 4 ad2antrr 
 |-  ( ( ( ph /\ ( x e. Y /\ w e. Y ) ) /\ ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) ) -> U e. CPreHil )
14 5 ad2antrr 
 |-  ( ( ( ph /\ ( x e. Y /\ w e. Y ) ) /\ ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) ) -> Y e. ( LSubSp ` U ) )
15 6 ad2antrr 
 |-  ( ( ( ph /\ ( x e. Y /\ w e. Y ) ) /\ ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) ) -> ( U |`s Y ) e. CMetSp )
16 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 )
17 0re 
 |-  0 e. RR
18 17 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 )
19 0le0 
 |-  0 <_ 0
20 19 a1i 
 |-  ( ( ( ph /\ ( x e. Y /\ w e. Y ) ) /\ ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) /\ ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) ) ) -> 0 <_ 0 )
21 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 )
22 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 )
23 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 ) )
24 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 ) )
25 1 2 3 13 14 15 16 8 9 10 11 18 20 21 22 23 24 minveclem2 
 |-  ( ( ( 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 25 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 ) ) )
27 1 2 3 4 5 6 7 8 9 10 11 minveclem6 
 |-  ( ( ph /\ x e. Y ) -> ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) )
28 27 adantrr 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) )
29 1 2 3 4 5 6 7 8 9 10 11 minveclem6 
 |-  ( ( ph /\ w e. Y ) -> ( ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. y e. Y ( N ` ( A .- w ) ) <_ ( N ` ( A .- y ) ) ) )
30 29 adantrl 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( ( A D w ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. y e. Y ( N ` ( A .- w ) ) <_ ( N ` ( A .- y ) ) ) )
31 28 30 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 .- x ) ) <_ ( N ` ( A .- y ) ) /\ A. y e. Y ( N ` ( A .- w ) ) <_ ( N ` ( A .- y ) ) ) ) )
32 4cn 
 |-  4 e. CC
33 32 mul01i 
 |-  ( 4 x. 0 ) = 0
34 33 breq2i 
 |-  ( ( ( x D w ) ^ 2 ) <_ ( 4 x. 0 ) <-> ( ( x D w ) ^ 2 ) <_ 0 )
35 cphngp 
 |-  ( U e. CPreHil -> U e. NrmGrp )
36 ngpms 
 |-  ( U e. NrmGrp -> U e. MetSp )
37 4 35 36 3syl 
 |-  ( ph -> U e. MetSp )
38 37 adantr 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> U e. MetSp )
39 1 11 msmet 
 |-  ( U e. MetSp -> D e. ( Met ` X ) )
40 38 39 syl 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> D e. ( Met ` X ) )
41 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
42 1 41 lssss 
 |-  ( Y e. ( LSubSp ` U ) -> Y C_ X )
43 5 42 syl 
 |-  ( 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 40 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 17 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 40 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 34 62 bitrid 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( ( x D w ) ^ 2 ) <_ ( 4 x. 0 ) <-> x = w ) )
64 26 31 63 3imtr3d 
 |-  ( ( ph /\ ( x e. Y /\ w e. Y ) ) -> ( ( A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) /\ A. y e. Y ( N ` ( A .- w ) ) <_ ( N ` ( A .- y ) ) ) -> x = w ) )
65 64 ralrimivva 
 |-  ( ph -> A. x e. Y A. w e. Y ( ( A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) /\ A. y e. Y ( N ` ( A .- w ) ) <_ ( N ` ( A .- y ) ) ) -> x = w ) )
66 oveq2 
 |-  ( x = w -> ( A .- x ) = ( A .- w ) )
67 66 fveq2d 
 |-  ( x = w -> ( N ` ( A .- x ) ) = ( N ` ( A .- w ) ) )
68 67 breq1d 
 |-  ( x = w -> ( ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) <-> ( N ` ( A .- w ) ) <_ ( N ` ( A .- y ) ) ) )
69 68 ralbidv 
 |-  ( x = w -> ( A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) <-> A. y e. Y ( N ` ( A .- w ) ) <_ ( N ` ( A .- y ) ) ) )
70 69 reu4 
 |-  ( E! x e. Y A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) <-> ( E. x e. Y A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) /\ A. x e. Y A. w e. Y ( ( A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) /\ A. y e. Y ( N ` ( A .- w ) ) <_ ( N ` ( A .- y ) ) ) -> x = w ) ) )
71 12 65 70 sylanbrc 
 |-  ( ph -> E! x e. Y A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) )