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 |
|
minveclem2.1 |
|- ( ph -> B e. RR ) |
13 |
|
minveclem2.2 |
|- ( ph -> 0 <_ B ) |
14 |
|
minveclem2.3 |
|- ( ph -> K e. Y ) |
15 |
|
minveclem2.4 |
|- ( ph -> L e. Y ) |
16 |
|
minveclem2.5 |
|- ( ph -> ( ( A D K ) ^ 2 ) <_ ( ( S ^ 2 ) + B ) ) |
17 |
|
minveclem2.6 |
|- ( ph -> ( ( A D L ) ^ 2 ) <_ ( ( S ^ 2 ) + B ) ) |
18 |
|
4re |
|- 4 e. RR |
19 |
1 2 3 4 5 6 7 8 9 10
|
minveclem4c |
|- ( ph -> S e. RR ) |
20 |
19
|
resqcld |
|- ( ph -> ( S ^ 2 ) e. RR ) |
21 |
|
remulcl |
|- ( ( 4 e. RR /\ ( S ^ 2 ) e. RR ) -> ( 4 x. ( S ^ 2 ) ) e. RR ) |
22 |
18 20 21
|
sylancr |
|- ( ph -> ( 4 x. ( S ^ 2 ) ) e. RR ) |
23 |
|
cphngp |
|- ( U e. CPreHil -> U e. NrmGrp ) |
24 |
4 23
|
syl |
|- ( ph -> U e. NrmGrp ) |
25 |
|
ngpms |
|- ( U e. NrmGrp -> U e. MetSp ) |
26 |
24 25
|
syl |
|- ( ph -> U e. MetSp ) |
27 |
1 11
|
msmet |
|- ( U e. MetSp -> D e. ( Met ` X ) ) |
28 |
26 27
|
syl |
|- ( ph -> D e. ( Met ` X ) ) |
29 |
|
eqid |
|- ( LSubSp ` U ) = ( LSubSp ` U ) |
30 |
1 29
|
lssss |
|- ( Y e. ( LSubSp ` U ) -> Y C_ X ) |
31 |
5 30
|
syl |
|- ( ph -> Y C_ X ) |
32 |
31 14
|
sseldd |
|- ( ph -> K e. X ) |
33 |
31 15
|
sseldd |
|- ( ph -> L e. X ) |
34 |
|
metcl |
|- ( ( D e. ( Met ` X ) /\ K e. X /\ L e. X ) -> ( K D L ) e. RR ) |
35 |
28 32 33 34
|
syl3anc |
|- ( ph -> ( K D L ) e. RR ) |
36 |
35
|
resqcld |
|- ( ph -> ( ( K D L ) ^ 2 ) e. RR ) |
37 |
22 36
|
readdcld |
|- ( ph -> ( ( 4 x. ( S ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) e. RR ) |
38 |
|
cphlmod |
|- ( U e. CPreHil -> U e. LMod ) |
39 |
4 38
|
syl |
|- ( ph -> U e. LMod ) |
40 |
|
cphclm |
|- ( U e. CPreHil -> U e. CMod ) |
41 |
4 40
|
syl |
|- ( ph -> U e. CMod ) |
42 |
|
eqid |
|- ( Scalar ` U ) = ( Scalar ` U ) |
43 |
|
eqid |
|- ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) ) |
44 |
42 43
|
clmzss |
|- ( U e. CMod -> ZZ C_ ( Base ` ( Scalar ` U ) ) ) |
45 |
41 44
|
syl |
|- ( ph -> ZZ C_ ( Base ` ( Scalar ` U ) ) ) |
46 |
|
2z |
|- 2 e. ZZ |
47 |
46
|
a1i |
|- ( ph -> 2 e. ZZ ) |
48 |
45 47
|
sseldd |
|- ( ph -> 2 e. ( Base ` ( Scalar ` U ) ) ) |
49 |
|
2ne0 |
|- 2 =/= 0 |
50 |
49
|
a1i |
|- ( ph -> 2 =/= 0 ) |
51 |
42 43
|
cphreccl |
|- ( ( U e. CPreHil /\ 2 e. ( Base ` ( Scalar ` U ) ) /\ 2 =/= 0 ) -> ( 1 / 2 ) e. ( Base ` ( Scalar ` U ) ) ) |
52 |
4 48 50 51
|
syl3anc |
|- ( ph -> ( 1 / 2 ) e. ( Base ` ( Scalar ` U ) ) ) |
53 |
|
eqid |
|- ( +g ` U ) = ( +g ` U ) |
54 |
53 29
|
lssvacl |
|- ( ( ( U e. LMod /\ Y e. ( LSubSp ` U ) ) /\ ( K e. Y /\ L e. Y ) ) -> ( K ( +g ` U ) L ) e. Y ) |
55 |
39 5 14 15 54
|
syl22anc |
|- ( ph -> ( K ( +g ` U ) L ) e. Y ) |
56 |
|
eqid |
|- ( .s ` U ) = ( .s ` U ) |
57 |
42 56 43 29
|
lssvscl |
|- ( ( ( U e. LMod /\ Y e. ( LSubSp ` U ) ) /\ ( ( 1 / 2 ) e. ( Base ` ( Scalar ` U ) ) /\ ( K ( +g ` U ) L ) e. Y ) ) -> ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) e. Y ) |
58 |
39 5 52 55 57
|
syl22anc |
|- ( ph -> ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) e. Y ) |
59 |
31 58
|
sseldd |
|- ( ph -> ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) e. X ) |
60 |
1 2
|
lmodvsubcl |
|- ( ( U e. LMod /\ A e. X /\ ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) e. X ) -> ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) e. X ) |
61 |
39 7 59 60
|
syl3anc |
|- ( ph -> ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) e. X ) |
62 |
1 3
|
nmcl |
|- ( ( U e. NrmGrp /\ ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) e. X ) -> ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) e. RR ) |
63 |
24 61 62
|
syl2anc |
|- ( ph -> ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) e. RR ) |
64 |
63
|
resqcld |
|- ( ph -> ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) e. RR ) |
65 |
|
remulcl |
|- ( ( 4 e. RR /\ ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) e. RR ) -> ( 4 x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) e. RR ) |
66 |
18 64 65
|
sylancr |
|- ( ph -> ( 4 x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) e. RR ) |
67 |
66 36
|
readdcld |
|- ( ph -> ( ( 4 x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) e. RR ) |
68 |
20 12
|
readdcld |
|- ( ph -> ( ( S ^ 2 ) + B ) e. RR ) |
69 |
|
remulcl |
|- ( ( 4 e. RR /\ ( ( S ^ 2 ) + B ) e. RR ) -> ( 4 x. ( ( S ^ 2 ) + B ) ) e. RR ) |
70 |
18 68 69
|
sylancr |
|- ( ph -> ( 4 x. ( ( S ^ 2 ) + B ) ) e. RR ) |
71 |
1 2 3 4 5 6 7 8 9
|
minveclem1 |
|- ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) ) |
72 |
71
|
simp3d |
|- ( ph -> A. w e. R 0 <_ w ) |
73 |
71
|
simp1d |
|- ( ph -> R C_ RR ) |
74 |
71
|
simp2d |
|- ( ph -> R =/= (/) ) |
75 |
|
0re |
|- 0 e. RR |
76 |
|
breq1 |
|- ( x = 0 -> ( x <_ w <-> 0 <_ w ) ) |
77 |
76
|
ralbidv |
|- ( x = 0 -> ( A. w e. R x <_ w <-> A. w e. R 0 <_ w ) ) |
78 |
77
|
rspcev |
|- ( ( 0 e. RR /\ A. w e. R 0 <_ w ) -> E. x e. RR A. w e. R x <_ w ) |
79 |
75 72 78
|
sylancr |
|- ( ph -> E. x e. RR A. w e. R x <_ w ) |
80 |
75
|
a1i |
|- ( ph -> 0 e. RR ) |
81 |
|
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 ) ) |
82 |
73 74 79 80 81
|
syl31anc |
|- ( ph -> ( 0 <_ inf ( R , RR , < ) <-> A. w e. R 0 <_ w ) ) |
83 |
72 82
|
mpbird |
|- ( ph -> 0 <_ inf ( R , RR , < ) ) |
84 |
83 10
|
breqtrrdi |
|- ( ph -> 0 <_ S ) |
85 |
|
eqid |
|- ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) = ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) |
86 |
|
oveq2 |
|- ( y = ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) -> ( A .- y ) = ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) |
87 |
86
|
fveq2d |
|- ( y = ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) -> ( N ` ( A .- y ) ) = ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) |
88 |
87
|
rspceeqv |
|- ( ( ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) e. Y /\ ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) = ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) -> E. y e. Y ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) = ( N ` ( A .- y ) ) ) |
89 |
58 85 88
|
sylancl |
|- ( ph -> E. y e. Y ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) = ( N ` ( A .- y ) ) ) |
90 |
|
eqid |
|- ( y e. Y |-> ( N ` ( A .- y ) ) ) = ( y e. Y |-> ( N ` ( A .- y ) ) ) |
91 |
|
fvex |
|- ( N ` ( A .- y ) ) e. _V |
92 |
90 91
|
elrnmpti |
|- ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) <-> E. y e. Y ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) = ( N ` ( A .- y ) ) ) |
93 |
89 92
|
sylibr |
|- ( ph -> ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) ) |
94 |
93 9
|
eleqtrrdi |
|- ( ph -> ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) e. R ) |
95 |
|
infrelb |
|- ( ( R C_ RR /\ E. x e. RR A. w e. R x <_ w /\ ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) e. R ) -> inf ( R , RR , < ) <_ ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) |
96 |
73 79 94 95
|
syl3anc |
|- ( ph -> inf ( R , RR , < ) <_ ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) |
97 |
10 96
|
eqbrtrid |
|- ( ph -> S <_ ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) |
98 |
|
le2sq2 |
|- ( ( ( S e. RR /\ 0 <_ S ) /\ ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) e. RR /\ S <_ ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) ) -> ( S ^ 2 ) <_ ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) |
99 |
19 84 63 97 98
|
syl22anc |
|- ( ph -> ( S ^ 2 ) <_ ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) |
100 |
|
4pos |
|- 0 < 4 |
101 |
18 100
|
pm3.2i |
|- ( 4 e. RR /\ 0 < 4 ) |
102 |
|
lemul2 |
|- ( ( ( S ^ 2 ) e. RR /\ ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) e. RR /\ ( 4 e. RR /\ 0 < 4 ) ) -> ( ( S ^ 2 ) <_ ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) <-> ( 4 x. ( S ^ 2 ) ) <_ ( 4 x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) ) ) |
103 |
101 102
|
mp3an3 |
|- ( ( ( S ^ 2 ) e. RR /\ ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) e. RR ) -> ( ( S ^ 2 ) <_ ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) <-> ( 4 x. ( S ^ 2 ) ) <_ ( 4 x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) ) ) |
104 |
20 64 103
|
syl2anc |
|- ( ph -> ( ( S ^ 2 ) <_ ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) <-> ( 4 x. ( S ^ 2 ) ) <_ ( 4 x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) ) ) |
105 |
99 104
|
mpbid |
|- ( ph -> ( 4 x. ( S ^ 2 ) ) <_ ( 4 x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) ) |
106 |
22 66 36 105
|
leadd1dd |
|- ( ph -> ( ( 4 x. ( S ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) <_ ( ( 4 x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) ) |
107 |
|
metcl |
|- ( ( D e. ( Met ` X ) /\ A e. X /\ K e. X ) -> ( A D K ) e. RR ) |
108 |
28 7 32 107
|
syl3anc |
|- ( ph -> ( A D K ) e. RR ) |
109 |
108
|
resqcld |
|- ( ph -> ( ( A D K ) ^ 2 ) e. RR ) |
110 |
|
metcl |
|- ( ( D e. ( Met ` X ) /\ A e. X /\ L e. X ) -> ( A D L ) e. RR ) |
111 |
28 7 33 110
|
syl3anc |
|- ( ph -> ( A D L ) e. RR ) |
112 |
111
|
resqcld |
|- ( ph -> ( ( A D L ) ^ 2 ) e. RR ) |
113 |
109 112 68 68 16 17
|
le2addd |
|- ( ph -> ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) <_ ( ( ( S ^ 2 ) + B ) + ( ( S ^ 2 ) + B ) ) ) |
114 |
68
|
recnd |
|- ( ph -> ( ( S ^ 2 ) + B ) e. CC ) |
115 |
114
|
2timesd |
|- ( ph -> ( 2 x. ( ( S ^ 2 ) + B ) ) = ( ( ( S ^ 2 ) + B ) + ( ( S ^ 2 ) + B ) ) ) |
116 |
113 115
|
breqtrrd |
|- ( ph -> ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) <_ ( 2 x. ( ( S ^ 2 ) + B ) ) ) |
117 |
109 112
|
readdcld |
|- ( ph -> ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) e. RR ) |
118 |
|
2re |
|- 2 e. RR |
119 |
|
remulcl |
|- ( ( 2 e. RR /\ ( ( S ^ 2 ) + B ) e. RR ) -> ( 2 x. ( ( S ^ 2 ) + B ) ) e. RR ) |
120 |
118 68 119
|
sylancr |
|- ( ph -> ( 2 x. ( ( S ^ 2 ) + B ) ) e. RR ) |
121 |
|
2pos |
|- 0 < 2 |
122 |
118 121
|
pm3.2i |
|- ( 2 e. RR /\ 0 < 2 ) |
123 |
|
lemul2 |
|- ( ( ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) e. RR /\ ( 2 x. ( ( S ^ 2 ) + B ) ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) <_ ( 2 x. ( ( S ^ 2 ) + B ) ) <-> ( 2 x. ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) ) <_ ( 2 x. ( 2 x. ( ( S ^ 2 ) + B ) ) ) ) ) |
124 |
122 123
|
mp3an3 |
|- ( ( ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) e. RR /\ ( 2 x. ( ( S ^ 2 ) + B ) ) e. RR ) -> ( ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) <_ ( 2 x. ( ( S ^ 2 ) + B ) ) <-> ( 2 x. ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) ) <_ ( 2 x. ( 2 x. ( ( S ^ 2 ) + B ) ) ) ) ) |
125 |
117 120 124
|
syl2anc |
|- ( ph -> ( ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) <_ ( 2 x. ( ( S ^ 2 ) + B ) ) <-> ( 2 x. ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) ) <_ ( 2 x. ( 2 x. ( ( S ^ 2 ) + B ) ) ) ) ) |
126 |
116 125
|
mpbid |
|- ( ph -> ( 2 x. ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) ) <_ ( 2 x. ( 2 x. ( ( S ^ 2 ) + B ) ) ) ) |
127 |
1 2
|
lmodvsubcl |
|- ( ( U e. LMod /\ A e. X /\ K e. X ) -> ( A .- K ) e. X ) |
128 |
39 7 32 127
|
syl3anc |
|- ( ph -> ( A .- K ) e. X ) |
129 |
1 2
|
lmodvsubcl |
|- ( ( U e. LMod /\ A e. X /\ L e. X ) -> ( A .- L ) e. X ) |
130 |
39 7 33 129
|
syl3anc |
|- ( ph -> ( A .- L ) e. X ) |
131 |
1 53 2 3
|
nmpar |
|- ( ( U e. CPreHil /\ ( A .- K ) e. X /\ ( A .- L ) e. X ) -> ( ( ( N ` ( ( A .- K ) ( +g ` U ) ( A .- L ) ) ) ^ 2 ) + ( ( N ` ( ( A .- K ) .- ( A .- L ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` ( A .- K ) ) ^ 2 ) + ( ( N ` ( A .- L ) ) ^ 2 ) ) ) ) |
132 |
4 128 130 131
|
syl3anc |
|- ( ph -> ( ( ( N ` ( ( A .- K ) ( +g ` U ) ( A .- L ) ) ) ^ 2 ) + ( ( N ` ( ( A .- K ) .- ( A .- L ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` ( A .- K ) ) ^ 2 ) + ( ( N ` ( A .- L ) ) ^ 2 ) ) ) ) |
133 |
|
2cn |
|- 2 e. CC |
134 |
63
|
recnd |
|- ( ph -> ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) e. CC ) |
135 |
|
sqmul |
|- ( ( 2 e. CC /\ ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) e. CC ) -> ( ( 2 x. ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) ) |
136 |
133 134 135
|
sylancr |
|- ( ph -> ( ( 2 x. ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) ) |
137 |
|
sq2 |
|- ( 2 ^ 2 ) = 4 |
138 |
137
|
oveq1i |
|- ( ( 2 ^ 2 ) x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) = ( 4 x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) |
139 |
136 138
|
eqtrdi |
|- ( ph -> ( ( 2 x. ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) ^ 2 ) = ( 4 x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) ) |
140 |
1 3 56 42 43
|
cphnmvs |
|- ( ( U e. CPreHil /\ 2 e. ( Base ` ( Scalar ` U ) ) /\ ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) e. X ) -> ( N ` ( 2 ( .s ` U ) ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) = ( ( abs ` 2 ) x. ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) ) |
141 |
4 48 61 140
|
syl3anc |
|- ( ph -> ( N ` ( 2 ( .s ` U ) ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) = ( ( abs ` 2 ) x. ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) ) |
142 |
|
0le2 |
|- 0 <_ 2 |
143 |
|
absid |
|- ( ( 2 e. RR /\ 0 <_ 2 ) -> ( abs ` 2 ) = 2 ) |
144 |
118 142 143
|
mp2an |
|- ( abs ` 2 ) = 2 |
145 |
144
|
oveq1i |
|- ( ( abs ` 2 ) x. ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) = ( 2 x. ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) |
146 |
141 145
|
eqtrdi |
|- ( ph -> ( N ` ( 2 ( .s ` U ) ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) = ( 2 x. ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) ) |
147 |
1 56 42 43 2 39 48 7 59
|
lmodsubdi |
|- ( ph -> ( 2 ( .s ` U ) ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) = ( ( 2 ( .s ` U ) A ) .- ( 2 ( .s ` U ) ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) |
148 |
|
eqid |
|- ( .g ` U ) = ( .g ` U ) |
149 |
1 148 53
|
mulg2 |
|- ( A e. X -> ( 2 ( .g ` U ) A ) = ( A ( +g ` U ) A ) ) |
150 |
7 149
|
syl |
|- ( ph -> ( 2 ( .g ` U ) A ) = ( A ( +g ` U ) A ) ) |
151 |
1 148 56
|
clmmulg |
|- ( ( U e. CMod /\ 2 e. ZZ /\ A e. X ) -> ( 2 ( .g ` U ) A ) = ( 2 ( .s ` U ) A ) ) |
152 |
41 47 7 151
|
syl3anc |
|- ( ph -> ( 2 ( .g ` U ) A ) = ( 2 ( .s ` U ) A ) ) |
153 |
150 152
|
eqtr3d |
|- ( ph -> ( A ( +g ` U ) A ) = ( 2 ( .s ` U ) A ) ) |
154 |
1 53
|
lmodvacl |
|- ( ( U e. LMod /\ K e. X /\ L e. X ) -> ( K ( +g ` U ) L ) e. X ) |
155 |
39 32 33 154
|
syl3anc |
|- ( ph -> ( K ( +g ` U ) L ) e. X ) |
156 |
1 56
|
clmvs1 |
|- ( ( U e. CMod /\ ( K ( +g ` U ) L ) e. X ) -> ( 1 ( .s ` U ) ( K ( +g ` U ) L ) ) = ( K ( +g ` U ) L ) ) |
157 |
41 155 156
|
syl2anc |
|- ( ph -> ( 1 ( .s ` U ) ( K ( +g ` U ) L ) ) = ( K ( +g ` U ) L ) ) |
158 |
133 49
|
recidi |
|- ( 2 x. ( 1 / 2 ) ) = 1 |
159 |
158
|
oveq1i |
|- ( ( 2 x. ( 1 / 2 ) ) ( .s ` U ) ( K ( +g ` U ) L ) ) = ( 1 ( .s ` U ) ( K ( +g ` U ) L ) ) |
160 |
1 42 56 43
|
clmvsass |
|- ( ( U e. CMod /\ ( 2 e. ( Base ` ( Scalar ` U ) ) /\ ( 1 / 2 ) e. ( Base ` ( Scalar ` U ) ) /\ ( K ( +g ` U ) L ) e. X ) ) -> ( ( 2 x. ( 1 / 2 ) ) ( .s ` U ) ( K ( +g ` U ) L ) ) = ( 2 ( .s ` U ) ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) |
161 |
41 48 52 155 160
|
syl13anc |
|- ( ph -> ( ( 2 x. ( 1 / 2 ) ) ( .s ` U ) ( K ( +g ` U ) L ) ) = ( 2 ( .s ` U ) ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) |
162 |
159 161
|
syl5eqr |
|- ( ph -> ( 1 ( .s ` U ) ( K ( +g ` U ) L ) ) = ( 2 ( .s ` U ) ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) |
163 |
157 162
|
eqtr3d |
|- ( ph -> ( K ( +g ` U ) L ) = ( 2 ( .s ` U ) ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) |
164 |
153 163
|
oveq12d |
|- ( ph -> ( ( A ( +g ` U ) A ) .- ( K ( +g ` U ) L ) ) = ( ( 2 ( .s ` U ) A ) .- ( 2 ( .s ` U ) ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) |
165 |
|
lmodabl |
|- ( U e. LMod -> U e. Abel ) |
166 |
39 165
|
syl |
|- ( ph -> U e. Abel ) |
167 |
1 53 2
|
ablsub4 |
|- ( ( U e. Abel /\ ( A e. X /\ A e. X ) /\ ( K e. X /\ L e. X ) ) -> ( ( A ( +g ` U ) A ) .- ( K ( +g ` U ) L ) ) = ( ( A .- K ) ( +g ` U ) ( A .- L ) ) ) |
168 |
166 7 7 32 33 167
|
syl122anc |
|- ( ph -> ( ( A ( +g ` U ) A ) .- ( K ( +g ` U ) L ) ) = ( ( A .- K ) ( +g ` U ) ( A .- L ) ) ) |
169 |
147 164 168
|
3eqtr2d |
|- ( ph -> ( 2 ( .s ` U ) ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) = ( ( A .- K ) ( +g ` U ) ( A .- L ) ) ) |
170 |
169
|
fveq2d |
|- ( ph -> ( N ` ( 2 ( .s ` U ) ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) = ( N ` ( ( A .- K ) ( +g ` U ) ( A .- L ) ) ) ) |
171 |
146 170
|
eqtr3d |
|- ( ph -> ( 2 x. ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) = ( N ` ( ( A .- K ) ( +g ` U ) ( A .- L ) ) ) ) |
172 |
171
|
oveq1d |
|- ( ph -> ( ( 2 x. ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ) ^ 2 ) = ( ( N ` ( ( A .- K ) ( +g ` U ) ( A .- L ) ) ) ^ 2 ) ) |
173 |
139 172
|
eqtr3d |
|- ( ph -> ( 4 x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) = ( ( N ` ( ( A .- K ) ( +g ` U ) ( A .- L ) ) ) ^ 2 ) ) |
174 |
|
eqid |
|- ( dist ` U ) = ( dist ` U ) |
175 |
3 1 2 174
|
ngpdsr |
|- ( ( U e. NrmGrp /\ K e. X /\ L e. X ) -> ( K ( dist ` U ) L ) = ( N ` ( L .- K ) ) ) |
176 |
24 32 33 175
|
syl3anc |
|- ( ph -> ( K ( dist ` U ) L ) = ( N ` ( L .- K ) ) ) |
177 |
11
|
oveqi |
|- ( K D L ) = ( K ( ( dist ` U ) |` ( X X. X ) ) L ) |
178 |
32 33
|
ovresd |
|- ( ph -> ( K ( ( dist ` U ) |` ( X X. X ) ) L ) = ( K ( dist ` U ) L ) ) |
179 |
177 178
|
syl5eq |
|- ( ph -> ( K D L ) = ( K ( dist ` U ) L ) ) |
180 |
1 2 166 7 32 33
|
ablnnncan1 |
|- ( ph -> ( ( A .- K ) .- ( A .- L ) ) = ( L .- K ) ) |
181 |
180
|
fveq2d |
|- ( ph -> ( N ` ( ( A .- K ) .- ( A .- L ) ) ) = ( N ` ( L .- K ) ) ) |
182 |
176 179 181
|
3eqtr4d |
|- ( ph -> ( K D L ) = ( N ` ( ( A .- K ) .- ( A .- L ) ) ) ) |
183 |
182
|
oveq1d |
|- ( ph -> ( ( K D L ) ^ 2 ) = ( ( N ` ( ( A .- K ) .- ( A .- L ) ) ) ^ 2 ) ) |
184 |
173 183
|
oveq12d |
|- ( ph -> ( ( 4 x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) = ( ( ( N ` ( ( A .- K ) ( +g ` U ) ( A .- L ) ) ) ^ 2 ) + ( ( N ` ( ( A .- K ) .- ( A .- L ) ) ) ^ 2 ) ) ) |
185 |
11
|
oveqi |
|- ( A D K ) = ( A ( ( dist ` U ) |` ( X X. X ) ) K ) |
186 |
7 32
|
ovresd |
|- ( ph -> ( A ( ( dist ` U ) |` ( X X. X ) ) K ) = ( A ( dist ` U ) K ) ) |
187 |
185 186
|
syl5eq |
|- ( ph -> ( A D K ) = ( A ( dist ` U ) K ) ) |
188 |
3 1 2 174
|
ngpds |
|- ( ( U e. NrmGrp /\ A e. X /\ K e. X ) -> ( A ( dist ` U ) K ) = ( N ` ( A .- K ) ) ) |
189 |
24 7 32 188
|
syl3anc |
|- ( ph -> ( A ( dist ` U ) K ) = ( N ` ( A .- K ) ) ) |
190 |
187 189
|
eqtrd |
|- ( ph -> ( A D K ) = ( N ` ( A .- K ) ) ) |
191 |
190
|
oveq1d |
|- ( ph -> ( ( A D K ) ^ 2 ) = ( ( N ` ( A .- K ) ) ^ 2 ) ) |
192 |
11
|
oveqi |
|- ( A D L ) = ( A ( ( dist ` U ) |` ( X X. X ) ) L ) |
193 |
7 33
|
ovresd |
|- ( ph -> ( A ( ( dist ` U ) |` ( X X. X ) ) L ) = ( A ( dist ` U ) L ) ) |
194 |
192 193
|
syl5eq |
|- ( ph -> ( A D L ) = ( A ( dist ` U ) L ) ) |
195 |
3 1 2 174
|
ngpds |
|- ( ( U e. NrmGrp /\ A e. X /\ L e. X ) -> ( A ( dist ` U ) L ) = ( N ` ( A .- L ) ) ) |
196 |
24 7 33 195
|
syl3anc |
|- ( ph -> ( A ( dist ` U ) L ) = ( N ` ( A .- L ) ) ) |
197 |
194 196
|
eqtrd |
|- ( ph -> ( A D L ) = ( N ` ( A .- L ) ) ) |
198 |
197
|
oveq1d |
|- ( ph -> ( ( A D L ) ^ 2 ) = ( ( N ` ( A .- L ) ) ^ 2 ) ) |
199 |
191 198
|
oveq12d |
|- ( ph -> ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) = ( ( ( N ` ( A .- K ) ) ^ 2 ) + ( ( N ` ( A .- L ) ) ^ 2 ) ) ) |
200 |
199
|
oveq2d |
|- ( ph -> ( 2 x. ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) ) = ( 2 x. ( ( ( N ` ( A .- K ) ) ^ 2 ) + ( ( N ` ( A .- L ) ) ^ 2 ) ) ) ) |
201 |
132 184 200
|
3eqtr4d |
|- ( ph -> ( ( 4 x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) = ( 2 x. ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) ) ) |
202 |
|
2t2e4 |
|- ( 2 x. 2 ) = 4 |
203 |
202
|
oveq1i |
|- ( ( 2 x. 2 ) x. ( ( S ^ 2 ) + B ) ) = ( 4 x. ( ( S ^ 2 ) + B ) ) |
204 |
|
2cnd |
|- ( ph -> 2 e. CC ) |
205 |
204 204 114
|
mulassd |
|- ( ph -> ( ( 2 x. 2 ) x. ( ( S ^ 2 ) + B ) ) = ( 2 x. ( 2 x. ( ( S ^ 2 ) + B ) ) ) ) |
206 |
203 205
|
syl5eqr |
|- ( ph -> ( 4 x. ( ( S ^ 2 ) + B ) ) = ( 2 x. ( 2 x. ( ( S ^ 2 ) + B ) ) ) ) |
207 |
126 201 206
|
3brtr4d |
|- ( ph -> ( ( 4 x. ( ( N ` ( A .- ( ( 1 / 2 ) ( .s ` U ) ( K ( +g ` U ) L ) ) ) ) ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) <_ ( 4 x. ( ( S ^ 2 ) + B ) ) ) |
208 |
37 67 70 106 207
|
letrd |
|- ( ph -> ( ( 4 x. ( S ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) <_ ( 4 x. ( ( S ^ 2 ) + B ) ) ) |
209 |
|
4cn |
|- 4 e. CC |
210 |
209
|
a1i |
|- ( ph -> 4 e. CC ) |
211 |
20
|
recnd |
|- ( ph -> ( S ^ 2 ) e. CC ) |
212 |
12
|
recnd |
|- ( ph -> B e. CC ) |
213 |
210 211 212
|
adddid |
|- ( ph -> ( 4 x. ( ( S ^ 2 ) + B ) ) = ( ( 4 x. ( S ^ 2 ) ) + ( 4 x. B ) ) ) |
214 |
208 213
|
breqtrd |
|- ( ph -> ( ( 4 x. ( S ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) <_ ( ( 4 x. ( S ^ 2 ) ) + ( 4 x. B ) ) ) |
215 |
|
remulcl |
|- ( ( 4 e. RR /\ B e. RR ) -> ( 4 x. B ) e. RR ) |
216 |
18 12 215
|
sylancr |
|- ( ph -> ( 4 x. B ) e. RR ) |
217 |
36 216 22
|
leadd2d |
|- ( ph -> ( ( ( K D L ) ^ 2 ) <_ ( 4 x. B ) <-> ( ( 4 x. ( S ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) <_ ( ( 4 x. ( S ^ 2 ) ) + ( 4 x. B ) ) ) ) |
218 |
214 217
|
mpbird |
|- ( ph -> ( ( K D L ) ^ 2 ) <_ ( 4 x. B ) ) |