Metamath Proof Explorer

Theorem minveclem2

Description: Lemma for minvec . Any two points K and L in Y are close to each other if they are close to the infimum of distance to A . (Contributed by Mario Carneiro, 9-May-2014) (Revised by Mario Carneiro, 15-Oct-2015) (Revised by AV, 3-Oct-2020)

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 ) )
minveclem2.1 
|- ( ph -> B e. RR )
minveclem2.2 
|- ( ph -> 0 <_ B )
minveclem2.3 
|- ( ph -> K e. Y )
minveclem2.4 
|- ( ph -> L e. Y )
minveclem2.5 
|- ( ph -> ( ( A D K ) ^ 2 ) <_ ( ( S ^ 2 ) + B ) )
minveclem2.6 
|- ( ph -> ( ( A D L ) ^ 2 ) <_ ( ( S ^ 2 ) + B ) )
Assertion minveclem2 
|- ( ph -> ( ( K D L ) ^ 2 ) <_ ( 4 x. B ) )

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