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 |
11
|
oveqi |
|- ( A D x ) = ( A ( ( dist ` U ) |` ( X X. X ) ) x ) |
13 |
7
|
adantr |
|- ( ( ph /\ x e. Y ) -> A e. X ) |
14 |
|
eqid |
|- ( LSubSp ` U ) = ( LSubSp ` U ) |
15 |
1 14
|
lssss |
|- ( Y e. ( LSubSp ` U ) -> Y C_ X ) |
16 |
5 15
|
syl |
|- ( ph -> Y C_ X ) |
17 |
16
|
sselda |
|- ( ( ph /\ x e. Y ) -> x e. X ) |
18 |
13 17
|
ovresd |
|- ( ( ph /\ x e. Y ) -> ( A ( ( dist ` U ) |` ( X X. X ) ) x ) = ( A ( dist ` U ) x ) ) |
19 |
12 18
|
syl5eq |
|- ( ( ph /\ x e. Y ) -> ( A D x ) = ( A ( dist ` U ) x ) ) |
20 |
|
cphngp |
|- ( U e. CPreHil -> U e. NrmGrp ) |
21 |
4 20
|
syl |
|- ( ph -> U e. NrmGrp ) |
22 |
21
|
adantr |
|- ( ( ph /\ x e. Y ) -> U e. NrmGrp ) |
23 |
|
eqid |
|- ( dist ` U ) = ( dist ` U ) |
24 |
3 1 2 23
|
ngpds |
|- ( ( U e. NrmGrp /\ A e. X /\ x e. X ) -> ( A ( dist ` U ) x ) = ( N ` ( A .- x ) ) ) |
25 |
22 13 17 24
|
syl3anc |
|- ( ( ph /\ x e. Y ) -> ( A ( dist ` U ) x ) = ( N ` ( A .- x ) ) ) |
26 |
19 25
|
eqtrd |
|- ( ( ph /\ x e. Y ) -> ( A D x ) = ( N ` ( A .- x ) ) ) |
27 |
26
|
oveq1d |
|- ( ( ph /\ x e. Y ) -> ( ( A D x ) ^ 2 ) = ( ( N ` ( A .- x ) ) ^ 2 ) ) |
28 |
1 2 3 4 5 6 7 8 9
|
minveclem1 |
|- ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) ) |
29 |
28
|
adantr |
|- ( ( ph /\ x e. Y ) -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) ) |
30 |
29
|
simp1d |
|- ( ( ph /\ x e. Y ) -> R C_ RR ) |
31 |
29
|
simp2d |
|- ( ( ph /\ x e. Y ) -> R =/= (/) ) |
32 |
|
0red |
|- ( ( ph /\ x e. Y ) -> 0 e. RR ) |
33 |
29
|
simp3d |
|- ( ( ph /\ x e. Y ) -> A. w e. R 0 <_ w ) |
34 |
|
breq1 |
|- ( x = 0 -> ( x <_ w <-> 0 <_ w ) ) |
35 |
34
|
ralbidv |
|- ( x = 0 -> ( A. w e. R x <_ w <-> A. w e. R 0 <_ w ) ) |
36 |
35
|
rspcev |
|- ( ( 0 e. RR /\ A. w e. R 0 <_ w ) -> E. x e. RR A. w e. R x <_ w ) |
37 |
32 33 36
|
syl2anc |
|- ( ( ph /\ x e. Y ) -> E. x e. RR A. w e. R x <_ w ) |
38 |
|
infrecl |
|- ( ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) -> inf ( R , RR , < ) e. RR ) |
39 |
30 31 37 38
|
syl3anc |
|- ( ( ph /\ x e. Y ) -> inf ( R , RR , < ) e. RR ) |
40 |
10 39
|
eqeltrid |
|- ( ( ph /\ x e. Y ) -> S e. RR ) |
41 |
40
|
resqcld |
|- ( ( ph /\ x e. Y ) -> ( S ^ 2 ) e. RR ) |
42 |
41
|
recnd |
|- ( ( ph /\ x e. Y ) -> ( S ^ 2 ) e. CC ) |
43 |
42
|
addid1d |
|- ( ( ph /\ x e. Y ) -> ( ( S ^ 2 ) + 0 ) = ( S ^ 2 ) ) |
44 |
27 43
|
breq12d |
|- ( ( ph /\ x e. Y ) -> ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> ( ( N ` ( A .- x ) ) ^ 2 ) <_ ( S ^ 2 ) ) ) |
45 |
|
cphlmod |
|- ( U e. CPreHil -> U e. LMod ) |
46 |
4 45
|
syl |
|- ( ph -> U e. LMod ) |
47 |
46
|
adantr |
|- ( ( ph /\ x e. Y ) -> U e. LMod ) |
48 |
1 2
|
lmodvsubcl |
|- ( ( U e. LMod /\ A e. X /\ x e. X ) -> ( A .- x ) e. X ) |
49 |
47 13 17 48
|
syl3anc |
|- ( ( ph /\ x e. Y ) -> ( A .- x ) e. X ) |
50 |
1 3
|
nmcl |
|- ( ( U e. NrmGrp /\ ( A .- x ) e. X ) -> ( N ` ( A .- x ) ) e. RR ) |
51 |
22 49 50
|
syl2anc |
|- ( ( ph /\ x e. Y ) -> ( N ` ( A .- x ) ) e. RR ) |
52 |
1 3
|
nmge0 |
|- ( ( U e. NrmGrp /\ ( A .- x ) e. X ) -> 0 <_ ( N ` ( A .- x ) ) ) |
53 |
22 49 52
|
syl2anc |
|- ( ( ph /\ x e. Y ) -> 0 <_ ( N ` ( A .- x ) ) ) |
54 |
|
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 ) ) |
55 |
30 31 37 32 54
|
syl31anc |
|- ( ( ph /\ x e. Y ) -> ( 0 <_ inf ( R , RR , < ) <-> A. w e. R 0 <_ w ) ) |
56 |
33 55
|
mpbird |
|- ( ( ph /\ x e. Y ) -> 0 <_ inf ( R , RR , < ) ) |
57 |
56 10
|
breqtrrdi |
|- ( ( ph /\ x e. Y ) -> 0 <_ S ) |
58 |
51 40 53 57
|
le2sqd |
|- ( ( ph /\ x e. Y ) -> ( ( N ` ( A .- x ) ) <_ S <-> ( ( N ` ( A .- x ) ) ^ 2 ) <_ ( S ^ 2 ) ) ) |
59 |
10
|
breq2i |
|- ( ( N ` ( A .- x ) ) <_ S <-> ( N ` ( A .- x ) ) <_ inf ( R , RR , < ) ) |
60 |
|
infregelb |
|- ( ( ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) /\ ( N ` ( A .- x ) ) e. RR ) -> ( ( N ` ( A .- x ) ) <_ inf ( R , RR , < ) <-> A. w e. R ( N ` ( A .- x ) ) <_ w ) ) |
61 |
30 31 37 51 60
|
syl31anc |
|- ( ( ph /\ x e. Y ) -> ( ( N ` ( A .- x ) ) <_ inf ( R , RR , < ) <-> A. w e. R ( N ` ( A .- x ) ) <_ w ) ) |
62 |
59 61
|
syl5bb |
|- ( ( ph /\ x e. Y ) -> ( ( N ` ( A .- x ) ) <_ S <-> A. w e. R ( N ` ( A .- x ) ) <_ w ) ) |
63 |
44 58 62
|
3bitr2d |
|- ( ( ph /\ x e. Y ) -> ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. w e. R ( N ` ( A .- x ) ) <_ w ) ) |
64 |
9
|
raleqi |
|- ( A. w e. R ( N ` ( A .- x ) ) <_ w <-> A. w e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) ( N ` ( A .- x ) ) <_ w ) |
65 |
|
fvex |
|- ( N ` ( A .- y ) ) e. _V |
66 |
65
|
rgenw |
|- A. y e. Y ( N ` ( A .- y ) ) e. _V |
67 |
|
eqid |
|- ( y e. Y |-> ( N ` ( A .- y ) ) ) = ( y e. Y |-> ( N ` ( A .- y ) ) ) |
68 |
|
breq2 |
|- ( w = ( N ` ( A .- y ) ) -> ( ( N ` ( A .- x ) ) <_ w <-> ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) |
69 |
67 68
|
ralrnmptw |
|- ( A. y e. Y ( N ` ( A .- y ) ) e. _V -> ( A. w e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) ( N ` ( A .- x ) ) <_ w <-> A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) |
70 |
66 69
|
ax-mp |
|- ( A. w e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) ( N ` ( A .- x ) ) <_ w <-> A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) |
71 |
64 70
|
bitri |
|- ( A. w e. R ( N ` ( A .- x ) ) <_ w <-> A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) |
72 |
63 71
|
bitrdi |
|- ( ( ph /\ x e. Y ) -> ( ( ( A D x ) ^ 2 ) <_ ( ( S ^ 2 ) + 0 ) <-> A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) ) ) |