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