Metamath Proof Explorer

Theorem minvecolem2

Description: Lemma for minveco . 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 AV, 4-Oct-2020) (New usage is discouraged.)

Ref Expression
Hypotheses minveco.x 
|- X = ( BaseSet ` U )
minveco.m 
|- M = ( -v ` U )
minveco.n 
|- N = ( normCV ` U )
minveco.y 
|- Y = ( BaseSet ` W )
minveco.u 
|- ( ph -> U e. CPreHilOLD )
minveco.w 
|- ( ph -> W e. ( ( SubSp ` U ) i^i CBan ) )
minveco.a 
|- ( ph -> A e. X )
minveco.d 
|- D = ( IndMet ` U )
minveco.j 
|- J = ( MetOpen ` D )
minveco.r 
|- R = ran ( y e. Y |-> ( N ` ( A M y ) ) )
minveco.s 
|- S = inf ( R , RR , < )
minvecolem2.1 
|- ( ph -> B e. RR )
minvecolem2.2 
|- ( ph -> 0 <_ B )
minvecolem2.3 
|- ( ph -> K e. Y )
minvecolem2.4 
|- ( ph -> L e. Y )
minvecolem2.5 
|- ( ph -> ( ( A D K ) ^ 2 ) <_ ( ( S ^ 2 ) + B ) )
minvecolem2.6 
|- ( ph -> ( ( A D L ) ^ 2 ) <_ ( ( S ^ 2 ) + B ) )
Assertion minvecolem2 
|- ( ph -> ( ( K D L ) ^ 2 ) <_ ( 4 x. B ) )

Proof

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 minvecolem2.1 
 |-  ( ph -> B e. RR )
13 minvecolem2.2 
 |-  ( ph -> 0 <_ B )
14 minvecolem2.3 
 |-  ( ph -> K e. Y )
15 minvecolem2.4 
 |-  ( ph -> L e. Y )
16 minvecolem2.5 
 |-  ( ph -> ( ( A D K ) ^ 2 ) <_ ( ( S ^ 2 ) + B ) )
17 minvecolem2.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 minvecolem1 
 |-  ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )
20 19 simp1d 
 |-  ( ph -> R C_ RR )
21 19 simp2d 
 |-  ( ph -> R =/= (/) )
22 0re 
 |-  0 e. RR
23 19 simp3d 
 |-  ( ph -> A. w e. R 0 <_ w )
24 breq1 
 |-  ( x = 0 -> ( x <_ w <-> 0 <_ w ) )
25 24 ralbidv 
 |-  ( x = 0 -> ( A. w e. R x <_ w <-> A. w e. R 0 <_ w ) )
26 25 rspcev 
 |-  ( ( 0 e. RR /\ A. w e. R 0 <_ w ) -> E. x e. RR A. w e. R x <_ w )
27 22 23 26 sylancr 
 |-  ( ph -> E. x e. RR A. w e. R x <_ w )
28 infrecl 
 |-  ( ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) -> inf ( R , RR , < ) e. RR )
29 20 21 27 28 syl3anc 
 |-  ( ph -> inf ( R , RR , < ) e. RR )
30 11 29 eqeltrid 
 |-  ( ph -> S e. RR )
31 30 resqcld 
 |-  ( ph -> ( S ^ 2 ) e. RR )
32 remulcl 
 |-  ( ( 4 e. RR /\ ( S ^ 2 ) e. RR ) -> ( 4 x. ( S ^ 2 ) ) e. RR )
33 18 31 32 sylancr 
 |-  ( ph -> ( 4 x. ( S ^ 2 ) ) e. RR )
34 phnv 
 |-  ( U e. CPreHilOLD -> U e. NrmCVec )
35 5 34 syl 
 |-  ( ph -> U e. NrmCVec )
36 1 8 imsmet 
 |-  ( U e. NrmCVec -> D e. ( Met ` X ) )
37 35 36 syl 
 |-  ( ph -> D e. ( Met ` X ) )
38 inss1 
 |-  ( ( SubSp ` U ) i^i CBan ) C_ ( SubSp ` U )
39 38 6 sselid 
 |-  ( ph -> W e. ( SubSp ` U ) )
40 eqid 
 |-  ( SubSp ` U ) = ( SubSp ` U )
41 1 4 40 sspba 
 |-  ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) -> Y C_ X )
42 35 39 41 syl2anc 
 |-  ( ph -> Y C_ X )
43 42 14 sseldd 
 |-  ( ph -> K e. X )
44 42 15 sseldd 
 |-  ( ph -> L e. X )
45 metcl 
 |-  ( ( D e. ( Met ` X ) /\ K e. X /\ L e. X ) -> ( K D L ) e. RR )
46 37 43 44 45 syl3anc 
 |-  ( ph -> ( K D L ) e. RR )
47 46 resqcld 
 |-  ( ph -> ( ( K D L ) ^ 2 ) e. RR )
48 33 47 readdcld 
 |-  ( ph -> ( ( 4 x. ( S ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) e. RR )
49 ax-1cn 
 |-  1 e. CC
50 halfcl 
 |-  ( 1 e. CC -> ( 1 / 2 ) e. CC )
51 49 50 mp1i 
 |-  ( ph -> ( 1 / 2 ) e. CC )
52 eqid 
 |-  ( +v ` U ) = ( +v ` U )
53 eqid 
 |-  ( +v ` W ) = ( +v ` W )
54 4 52 53 40 sspgval 
 |-  ( ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) /\ ( K e. Y /\ L e. Y ) ) -> ( K ( +v ` W ) L ) = ( K ( +v ` U ) L ) )
55 35 39 14 15 54 syl22anc 
 |-  ( ph -> ( K ( +v ` W ) L ) = ( K ( +v ` U ) L ) )
56 40 sspnv 
 |-  ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) -> W e. NrmCVec )
57 35 39 56 syl2anc 
 |-  ( ph -> W e. NrmCVec )
58 4 53 nvgcl 
 |-  ( ( W e. NrmCVec /\ K e. Y /\ L e. Y ) -> ( K ( +v ` W ) L ) e. Y )
59 57 14 15 58 syl3anc 
 |-  ( ph -> ( K ( +v ` W ) L ) e. Y )
60 55 59 eqeltrrd 
 |-  ( ph -> ( K ( +v ` U ) L ) e. Y )
61 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
62 eqid 
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
63 4 61 62 40 sspsval 
 |-  ( ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) /\ ( ( 1 / 2 ) e. CC /\ ( K ( +v ` U ) L ) e. Y ) ) -> ( ( 1 / 2 ) ( .sOLD ` W ) ( K ( +v ` U ) L ) ) = ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) )
64 35 39 51 60 63 syl22anc 
 |-  ( ph -> ( ( 1 / 2 ) ( .sOLD ` W ) ( K ( +v ` U ) L ) ) = ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) )
65 4 62 nvscl 
 |-  ( ( W e. NrmCVec /\ ( 1 / 2 ) e. CC /\ ( K ( +v ` U ) L ) e. Y ) -> ( ( 1 / 2 ) ( .sOLD ` W ) ( K ( +v ` U ) L ) ) e. Y )
66 57 51 60 65 syl3anc 
 |-  ( ph -> ( ( 1 / 2 ) ( .sOLD ` W ) ( K ( +v ` U ) L ) ) e. Y )
67 64 66 eqeltrrd 
 |-  ( ph -> ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) e. Y )
68 42 67 sseldd 
 |-  ( ph -> ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) e. X )
69 1 2 nvmcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) e. X ) -> ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) e. X )
70 35 7 68 69 syl3anc 
 |-  ( ph -> ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) e. X )
71 1 3 nvcl 
 |-  ( ( U e. NrmCVec /\ ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) e. X ) -> ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) e. RR )
72 35 70 71 syl2anc 
 |-  ( ph -> ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) e. RR )
73 72 resqcld 
 |-  ( ph -> ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) e. RR )
74 remulcl 
 |-  ( ( 4 e. RR /\ ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) e. RR ) -> ( 4 x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) ) e. RR )
75 18 73 74 sylancr 
 |-  ( ph -> ( 4 x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) ) e. RR )
76 75 47 readdcld 
 |-  ( ph -> ( ( 4 x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) e. RR )
77 31 12 readdcld 
 |-  ( ph -> ( ( S ^ 2 ) + B ) e. RR )
78 remulcl 
 |-  ( ( 4 e. RR /\ ( ( S ^ 2 ) + B ) e. RR ) -> ( 4 x. ( ( S ^ 2 ) + B ) ) e. RR )
79 18 77 78 sylancr 
 |-  ( ph -> ( 4 x. ( ( S ^ 2 ) + B ) ) e. RR )
80 22 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 20 21 27 80 81 syl31anc 
 |-  ( ph -> ( 0 <_ inf ( R , RR , < ) <-> A. w e. R 0 <_ w ) )
83 23 82 mpbird 
 |-  ( ph -> 0 <_ inf ( R , RR , < ) )
84 83 11 breqtrrdi 
 |-  ( ph -> 0 <_ S )
85 eqid 
 |-  ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) = ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) )
86 oveq2 
 |-  ( y = ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) -> ( A M y ) = ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) )
87 86 fveq2d 
 |-  ( y = ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) -> ( N ` ( A M y ) ) = ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) )
88 87 rspceeqv 
 |-  ( ( ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) e. Y /\ ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) = ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ) -> E. y e. Y ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) = ( N ` ( A M y ) ) )
89 67 85 88 sylancl 
 |-  ( ph -> E. y e. Y ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) = ( N ` ( A M y ) ) )
90 eqid 
 |-  ( y e. Y |-> ( N ` ( A M y ) ) ) = ( y e. Y |-> ( N ` ( A M y ) ) )
91 fvex 
 |-  ( N ` ( A M y ) ) e. _V
92 90 91 elrnmpti 
 |-  ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) e. ran ( y e. Y |-> ( N ` ( A M y ) ) ) <-> E. y e. Y ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) = ( N ` ( A M y ) ) )
93 89 92 sylibr 
 |-  ( ph -> ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) e. ran ( y e. Y |-> ( N ` ( A M y ) ) ) )
94 93 10 eleqtrrdi 
 |-  ( ph -> ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) e. R )
95 infrelb 
 |-  ( ( R C_ RR /\ E. x e. RR A. w e. R x <_ w /\ ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) e. R ) -> inf ( R , RR , < ) <_ ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) )
96 20 27 94 95 syl3anc 
 |-  ( ph -> inf ( R , RR , < ) <_ ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) )
97 11 96 eqbrtrid 
 |-  ( ph -> S <_ ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) )
98 le2sq2 
 |-  ( ( ( S e. RR /\ 0 <_ S ) /\ ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) e. RR /\ S <_ ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ) ) -> ( S ^ 2 ) <_ ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) )
99 30 84 72 97 98 syl22anc 
 |-  ( ph -> ( S ^ 2 ) <_ ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` 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 M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) e. RR /\ ( 4 e. RR /\ 0 < 4 ) ) -> ( ( S ^ 2 ) <_ ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) <-> ( 4 x. ( S ^ 2 ) ) <_ ( 4 x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) ) ) )
103 101 102 mp3an3 
 |-  ( ( ( S ^ 2 ) e. RR /\ ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) e. RR ) -> ( ( S ^ 2 ) <_ ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) <-> ( 4 x. ( S ^ 2 ) ) <_ ( 4 x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) ) ) )
104 31 73 103 syl2anc 
 |-  ( ph -> ( ( S ^ 2 ) <_ ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) <-> ( 4 x. ( S ^ 2 ) ) <_ ( 4 x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) ) ) )
105 99 104 mpbid 
 |-  ( ph -> ( 4 x. ( S ^ 2 ) ) <_ ( 4 x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) ) )
106 33 75 47 105 leadd1dd 
 |-  ( ph -> ( ( 4 x. ( S ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) <_ ( ( 4 x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` 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 37 7 43 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 37 7 44 110 syl3anc 
 |-  ( ph -> ( A D L ) e. RR )
112 111 resqcld 
 |-  ( ph -> ( ( A D L ) ^ 2 ) e. RR )
113 109 112 77 77 16 17 le2addd 
 |-  ( ph -> ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) <_ ( ( ( S ^ 2 ) + B ) + ( ( S ^ 2 ) + B ) ) )
114 77 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 77 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 nvmcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ K e. X ) -> ( A M K ) e. X )
128 35 7 43 127 syl3anc 
 |-  ( ph -> ( A M K ) e. X )
129 1 2 nvmcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ L e. X ) -> ( A M L ) e. X )
130 35 7 44 129 syl3anc 
 |-  ( ph -> ( A M L ) e. X )
131 1 52 2 3 phpar2 
 |-  ( ( U e. CPreHilOLD /\ ( A M K ) e. X /\ ( A M L ) e. X ) -> ( ( ( N ` ( ( A M K ) ( +v ` U ) ( A M L ) ) ) ^ 2 ) + ( ( N ` ( ( A M K ) M ( A M L ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` ( A M K ) ) ^ 2 ) + ( ( N ` ( A M L ) ) ^ 2 ) ) ) )
132 5 128 130 131 syl3anc 
 |-  ( ph -> ( ( ( N ` ( ( A M K ) ( +v ` U ) ( A M L ) ) ) ^ 2 ) + ( ( N ` ( ( A M K ) M ( A M L ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` ( A M K ) ) ^ 2 ) + ( ( N ` ( A M L ) ) ^ 2 ) ) ) )
133 2cn 
 |-  2 e. CC
134 72 recnd 
 |-  ( ph -> ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) e. CC )
135 sqmul 
 |-  ( ( 2 e. CC /\ ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) e. CC ) -> ( ( 2 x. ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) ) )
136 133 134 135 sylancr 
 |-  ( ph -> ( ( 2 x. ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) ) )
137 sq2 
 |-  ( 2 ^ 2 ) = 4
138 137 oveq1i 
 |-  ( ( 2 ^ 2 ) x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) ) = ( 4 x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) )
139 136 138 eqtrdi 
 |-  ( ph -> ( ( 2 x. ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ) ^ 2 ) = ( 4 x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) ) )
140 133 a1i 
 |-  ( ph -> 2 e. CC )
141 1 61 3 nvs 
 |-  ( ( U e. NrmCVec /\ 2 e. CC /\ ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) e. X ) -> ( N ` ( 2 ( .sOLD ` U ) ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ) = ( ( abs ` 2 ) x. ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ) )
142 35 140 70 141 syl3anc 
 |-  ( ph -> ( N ` ( 2 ( .sOLD ` U ) ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ) = ( ( abs ` 2 ) x. ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ) )
143 0le2 
 |-  0 <_ 2
144 absid 
 |-  ( ( 2 e. RR /\ 0 <_ 2 ) -> ( abs ` 2 ) = 2 )
145 118 143 144 mp2an 
 |-  ( abs ` 2 ) = 2
146 145 oveq1i 
 |-  ( ( abs ` 2 ) x. ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ) = ( 2 x. ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) )
147 142 146 eqtrdi 
 |-  ( ph -> ( N ` ( 2 ( .sOLD ` U ) ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ) = ( 2 x. ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ) )
148 1 2 61 nvmdi 
 |-  ( ( U e. NrmCVec /\ ( 2 e. CC /\ A e. X /\ ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) e. X ) ) -> ( 2 ( .sOLD ` U ) ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) = ( ( 2 ( .sOLD ` U ) A ) M ( 2 ( .sOLD ` U ) ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) )
149 35 140 7 68 148 syl13anc 
 |-  ( ph -> ( 2 ( .sOLD ` U ) ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) = ( ( 2 ( .sOLD ` U ) A ) M ( 2 ( .sOLD ` U ) ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) )
150 1 52 61 nv2 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( A ( +v ` U ) A ) = ( 2 ( .sOLD ` U ) A ) )
151 35 7 150 syl2anc 
 |-  ( ph -> ( A ( +v ` U ) A ) = ( 2 ( .sOLD ` U ) A ) )
152 2ne0 
 |-  2 =/= 0
153 133 152 recidi 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
154 153 oveq1i 
 |-  ( ( 2 x. ( 1 / 2 ) ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) = ( 1 ( .sOLD ` U ) ( K ( +v ` U ) L ) )
155 1 52 nvgcl 
 |-  ( ( U e. NrmCVec /\ K e. X /\ L e. X ) -> ( K ( +v ` U ) L ) e. X )
156 35 43 44 155 syl3anc 
 |-  ( ph -> ( K ( +v ` U ) L ) e. X )
157 1 61 nvsid 
 |-  ( ( U e. NrmCVec /\ ( K ( +v ` U ) L ) e. X ) -> ( 1 ( .sOLD ` U ) ( K ( +v ` U ) L ) ) = ( K ( +v ` U ) L ) )
158 35 156 157 syl2anc 
 |-  ( ph -> ( 1 ( .sOLD ` U ) ( K ( +v ` U ) L ) ) = ( K ( +v ` U ) L ) )
159 154 158 syl5eq 
 |-  ( ph -> ( ( 2 x. ( 1 / 2 ) ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) = ( K ( +v ` U ) L ) )
160 1 61 nvsass 
 |-  ( ( U e. NrmCVec /\ ( 2 e. CC /\ ( 1 / 2 ) e. CC /\ ( K ( +v ` U ) L ) e. X ) ) -> ( ( 2 x. ( 1 / 2 ) ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) = ( 2 ( .sOLD ` U ) ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) )
161 35 140 51 156 160 syl13anc 
 |-  ( ph -> ( ( 2 x. ( 1 / 2 ) ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) = ( 2 ( .sOLD ` U ) ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) )
162 159 161 eqtr3d 
 |-  ( ph -> ( K ( +v ` U ) L ) = ( 2 ( .sOLD ` U ) ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) )
163 151 162 oveq12d 
 |-  ( ph -> ( ( A ( +v ` U ) A ) M ( K ( +v ` U ) L ) ) = ( ( 2 ( .sOLD ` U ) A ) M ( 2 ( .sOLD ` U ) ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) )
164 1 52 2 nvaddsub4 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ A e. X ) /\ ( K e. X /\ L e. X ) ) -> ( ( A ( +v ` U ) A ) M ( K ( +v ` U ) L ) ) = ( ( A M K ) ( +v ` U ) ( A M L ) ) )
165 35 7 7 43 44 164 syl122anc 
 |-  ( ph -> ( ( A ( +v ` U ) A ) M ( K ( +v ` U ) L ) ) = ( ( A M K ) ( +v ` U ) ( A M L ) ) )
166 149 163 165 3eqtr2d 
 |-  ( ph -> ( 2 ( .sOLD ` U ) ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) = ( ( A M K ) ( +v ` U ) ( A M L ) ) )
167 166 fveq2d 
 |-  ( ph -> ( N ` ( 2 ( .sOLD ` U ) ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ) = ( N ` ( ( A M K ) ( +v ` U ) ( A M L ) ) ) )
168 147 167 eqtr3d 
 |-  ( ph -> ( 2 x. ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ) = ( N ` ( ( A M K ) ( +v ` U ) ( A M L ) ) ) )
169 168 oveq1d 
 |-  ( ph -> ( ( 2 x. ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ) ^ 2 ) = ( ( N ` ( ( A M K ) ( +v ` U ) ( A M L ) ) ) ^ 2 ) )
170 139 169 eqtr3d 
 |-  ( ph -> ( 4 x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) ) = ( ( N ` ( ( A M K ) ( +v ` U ) ( A M L ) ) ) ^ 2 ) )
171 1 2 3 8 imsdval 
 |-  ( ( U e. NrmCVec /\ L e. X /\ K e. X ) -> ( L D K ) = ( N ` ( L M K ) ) )
172 35 44 43 171 syl3anc 
 |-  ( ph -> ( L D K ) = ( N ` ( L M K ) ) )
173 metsym 
 |-  ( ( D e. ( Met ` X ) /\ K e. X /\ L e. X ) -> ( K D L ) = ( L D K ) )
174 37 43 44 173 syl3anc 
 |-  ( ph -> ( K D L ) = ( L D K ) )
175 1 2 nvnnncan1 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ K e. X /\ L e. X ) ) -> ( ( A M K ) M ( A M L ) ) = ( L M K ) )
176 35 7 43 44 175 syl13anc 
 |-  ( ph -> ( ( A M K ) M ( A M L ) ) = ( L M K ) )
177 176 fveq2d 
 |-  ( ph -> ( N ` ( ( A M K ) M ( A M L ) ) ) = ( N ` ( L M K ) ) )
178 172 174 177 3eqtr4d 
 |-  ( ph -> ( K D L ) = ( N ` ( ( A M K ) M ( A M L ) ) ) )
179 178 oveq1d 
 |-  ( ph -> ( ( K D L ) ^ 2 ) = ( ( N ` ( ( A M K ) M ( A M L ) ) ) ^ 2 ) )
180 170 179 oveq12d 
 |-  ( ph -> ( ( 4 x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) = ( ( ( N ` ( ( A M K ) ( +v ` U ) ( A M L ) ) ) ^ 2 ) + ( ( N ` ( ( A M K ) M ( A M L ) ) ) ^ 2 ) ) )
181 1 2 3 8 imsdval 
 |-  ( ( U e. NrmCVec /\ A e. X /\ K e. X ) -> ( A D K ) = ( N ` ( A M K ) ) )
182 35 7 43 181 syl3anc 
 |-  ( ph -> ( A D K ) = ( N ` ( A M K ) ) )
183 182 oveq1d 
 |-  ( ph -> ( ( A D K ) ^ 2 ) = ( ( N ` ( A M K ) ) ^ 2 ) )
184 1 2 3 8 imsdval 
 |-  ( ( U e. NrmCVec /\ A e. X /\ L e. X ) -> ( A D L ) = ( N ` ( A M L ) ) )
185 35 7 44 184 syl3anc 
 |-  ( ph -> ( A D L ) = ( N ` ( A M L ) ) )
186 185 oveq1d 
 |-  ( ph -> ( ( A D L ) ^ 2 ) = ( ( N ` ( A M L ) ) ^ 2 ) )
187 183 186 oveq12d 
 |-  ( ph -> ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) = ( ( ( N ` ( A M K ) ) ^ 2 ) + ( ( N ` ( A M L ) ) ^ 2 ) ) )
188 187 oveq2d 
 |-  ( ph -> ( 2 x. ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) ) = ( 2 x. ( ( ( N ` ( A M K ) ) ^ 2 ) + ( ( N ` ( A M L ) ) ^ 2 ) ) ) )
189 132 180 188 3eqtr4d 
 |-  ( ph -> ( ( 4 x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) = ( 2 x. ( ( ( A D K ) ^ 2 ) + ( ( A D L ) ^ 2 ) ) ) )
190 2t2e4 
 |-  ( 2 x. 2 ) = 4
191 190 oveq1i 
 |-  ( ( 2 x. 2 ) x. ( ( S ^ 2 ) + B ) ) = ( 4 x. ( ( S ^ 2 ) + B ) )
192 140 140 114 mulassd 
 |-  ( ph -> ( ( 2 x. 2 ) x. ( ( S ^ 2 ) + B ) ) = ( 2 x. ( 2 x. ( ( S ^ 2 ) + B ) ) ) )
193 191 192 eqtr3id 
 |-  ( ph -> ( 4 x. ( ( S ^ 2 ) + B ) ) = ( 2 x. ( 2 x. ( ( S ^ 2 ) + B ) ) ) )
194 126 189 193 3brtr4d 
 |-  ( ph -> ( ( 4 x. ( ( N ` ( A M ( ( 1 / 2 ) ( .sOLD ` U ) ( K ( +v ` U ) L ) ) ) ) ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) <_ ( 4 x. ( ( S ^ 2 ) + B ) ) )
195 48 76 79 106 194 letrd 
 |-  ( ph -> ( ( 4 x. ( S ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) <_ ( 4 x. ( ( S ^ 2 ) + B ) ) )
196 4cn 
 |-  4 e. CC
197 196 a1i 
 |-  ( ph -> 4 e. CC )
198 31 recnd 
 |-  ( ph -> ( S ^ 2 ) e. CC )
199 12 recnd 
 |-  ( ph -> B e. CC )
200 197 198 199 adddid 
 |-  ( ph -> ( 4 x. ( ( S ^ 2 ) + B ) ) = ( ( 4 x. ( S ^ 2 ) ) + ( 4 x. B ) ) )
201 195 200 breqtrd 
 |-  ( ph -> ( ( 4 x. ( S ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) <_ ( ( 4 x. ( S ^ 2 ) ) + ( 4 x. B ) ) )
202 remulcl 
 |-  ( ( 4 e. RR /\ B e. RR ) -> ( 4 x. B ) e. RR )
203 18 12 202 sylancr 
 |-  ( ph -> ( 4 x. B ) e. RR )
204 47 203 33 leadd2d 
 |-  ( ph -> ( ( ( K D L ) ^ 2 ) <_ ( 4 x. B ) <-> ( ( 4 x. ( S ^ 2 ) ) + ( ( K D L ) ^ 2 ) ) <_ ( ( 4 x. ( S ^ 2 ) ) + ( 4 x. B ) ) ) )
205 201 204 mpbird 
 |-  ( ph -> ( ( K D L ) ^ 2 ) <_ ( 4 x. B ) )