MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  minveclem2OLD Structured version   Visualization version   Unicode version

Theorem minveclem2OLD 22458
Description: Lemma for minvecOLD 22468. 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.) Obsolete version of minveclem2 22446 as of 3-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
minvecOLD.x  |-  X  =  ( Base `  U
)
minvecOLD.m  |-  .-  =  ( -g `  U )
minvecOLD.n  |-  N  =  ( norm `  U
)
minvecOLD.u  |-  ( ph  ->  U  e.  CPreHil )
minvecOLD.y  |-  ( ph  ->  Y  e.  ( LSubSp `  U ) )
minvecOLD.w  |-  ( ph  ->  ( Us  Y )  e. CMetSp )
minvecOLD.a  |-  ( ph  ->  A  e.  X )
minvecOLD.j  |-  J  =  ( TopOpen `  U )
minvecOLD.r  |-  R  =  ran  ( y  e.  Y  |->  ( N `  ( A  .-  y ) ) )
minvecOLD.s  |-  S  =  sup ( R ,  RR ,  `'  <  )
minvecOLD.d  |-  D  =  ( ( dist `  U
)  |`  ( X  X.  X ) )
minveclem2OLD.1  |-  ( ph  ->  B  e.  RR )
minveclem2OLD.2  |-  ( ph  ->  0  <_  B )
minveclem2OLD.3  |-  ( ph  ->  K  e.  Y )
minveclem2OLD.4  |-  ( ph  ->  L  e.  Y )
minveclem2OLD.5  |-  ( ph  ->  ( ( A D K ) ^ 2 )  <_  ( ( S ^ 2 )  +  B ) )
minveclem2OLD.6  |-  ( ph  ->  ( ( A D L ) ^ 2 )  <_  ( ( S ^ 2 )  +  B ) )
Assertion
Ref Expression
minveclem2OLD  |-  ( ph  ->  ( ( K D L ) ^ 2 )  <_  ( 4  x.  B ) )
Distinct variable groups:    y,  .-    y, A    y, J    y, K    y, N    ph, y    y, R    y, U    y, X    y, Y    y, D    y, S    y, L
Allowed substitution hint:    B( y)

Proof of Theorem minveclem2OLD
Dummy variables  w  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 4re 10708 . . . . . 6  |-  4  e.  RR
2 minvecOLD.x . . . . . . . 8  |-  X  =  ( Base `  U
)
3 minvecOLD.m . . . . . . . 8  |-  .-  =  ( -g `  U )
4 minvecOLD.n . . . . . . . 8  |-  N  =  ( norm `  U
)
5 minvecOLD.u . . . . . . . 8  |-  ( ph  ->  U  e.  CPreHil )
6 minvecOLD.y . . . . . . . 8  |-  ( ph  ->  Y  e.  ( LSubSp `  U ) )
7 minvecOLD.w . . . . . . . 8  |-  ( ph  ->  ( Us  Y )  e. CMetSp )
8 minvecOLD.a . . . . . . . 8  |-  ( ph  ->  A  e.  X )
9 minvecOLD.j . . . . . . . 8  |-  J  =  ( TopOpen `  U )
10 minvecOLD.r . . . . . . . 8  |-  R  =  ran  ( y  e.  Y  |->  ( N `  ( A  .-  y ) ) )
11 minvecOLD.s . . . . . . . 8  |-  S  =  sup ( R ,  RR ,  `'  <  )
122, 3, 4, 5, 6, 7, 8, 9, 10, 11minveclem4cOLD 22457 . . . . . . 7  |-  ( ph  ->  S  e.  RR )
1312resqcld 12480 . . . . . 6  |-  ( ph  ->  ( S ^ 2 )  e.  RR )
14 remulcl 9642 . . . . . 6  |-  ( ( 4  e.  RR  /\  ( S ^ 2 )  e.  RR )  -> 
( 4  x.  ( S ^ 2 ) )  e.  RR )
151, 13, 14sylancr 676 . . . . 5  |-  ( ph  ->  ( 4  x.  ( S ^ 2 ) )  e.  RR )
16 cphngp 22229 . . . . . . . . . 10  |-  ( U  e.  CPreHil  ->  U  e. NrmGrp )
175, 16syl 17 . . . . . . . . 9  |-  ( ph  ->  U  e. NrmGrp )
18 ngpms 21692 . . . . . . . . 9  |-  ( U  e. NrmGrp  ->  U  e.  MetSp )
1917, 18syl 17 . . . . . . . 8  |-  ( ph  ->  U  e.  MetSp )
20 minvecOLD.d . . . . . . . . 9  |-  D  =  ( ( dist `  U
)  |`  ( X  X.  X ) )
212, 20msmet 21550 . . . . . . . 8  |-  ( U  e.  MetSp  ->  D  e.  ( Met `  X ) )
2219, 21syl 17 . . . . . . 7  |-  ( ph  ->  D  e.  ( Met `  X ) )
23 eqid 2471 . . . . . . . . . 10  |-  ( LSubSp `  U )  =  (
LSubSp `  U )
242, 23lssss 18238 . . . . . . . . 9  |-  ( Y  e.  ( LSubSp `  U
)  ->  Y  C_  X
)
256, 24syl 17 . . . . . . . 8  |-  ( ph  ->  Y  C_  X )
26 minveclem2OLD.3 . . . . . . . 8  |-  ( ph  ->  K  e.  Y )
2725, 26sseldd 3419 . . . . . . 7  |-  ( ph  ->  K  e.  X )
28 minveclem2OLD.4 . . . . . . . 8  |-  ( ph  ->  L  e.  Y )
2925, 28sseldd 3419 . . . . . . 7  |-  ( ph  ->  L  e.  X )
30 metcl 21425 . . . . . . 7  |-  ( ( D  e.  ( Met `  X )  /\  K  e.  X  /\  L  e.  X )  ->  ( K D L )  e.  RR )
3122, 27, 29, 30syl3anc 1292 . . . . . 6  |-  ( ph  ->  ( K D L )  e.  RR )
3231resqcld 12480 . . . . 5  |-  ( ph  ->  ( ( K D L ) ^ 2 )  e.  RR )
3315, 32readdcld 9688 . . . 4  |-  ( ph  ->  ( ( 4  x.  ( S ^ 2 ) )  +  ( ( K D L ) ^ 2 ) )  e.  RR )
34 cphlmod 22230 . . . . . . . . . 10  |-  ( U  e.  CPreHil  ->  U  e.  LMod )
355, 34syl 17 . . . . . . . . 9  |-  ( ph  ->  U  e.  LMod )
36 cphclm 22245 . . . . . . . . . . . . . . 15  |-  ( U  e.  CPreHil  ->  U  e. CMod )
375, 36syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  U  e. CMod )
38 eqid 2471 . . . . . . . . . . . . . . 15  |-  (Scalar `  U )  =  (Scalar `  U )
39 eqid 2471 . . . . . . . . . . . . . . 15  |-  ( Base `  (Scalar `  U )
)  =  ( Base `  (Scalar `  U )
)
4038, 39clmzss 22187 . . . . . . . . . . . . . 14  |-  ( U  e. CMod  ->  ZZ  C_  ( Base `  (Scalar `  U
) ) )
4137, 40syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ZZ  C_  ( Base `  (Scalar `  U )
) )
42 2z 10993 . . . . . . . . . . . . . 14  |-  2  e.  ZZ
4342a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  2  e.  ZZ )
4441, 43sseldd 3419 . . . . . . . . . . . 12  |-  ( ph  ->  2  e.  ( Base `  (Scalar `  U )
) )
45 2ne0 10724 . . . . . . . . . . . . 13  |-  2  =/=  0
4645a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  2  =/=  0 )
4738, 39cphreccl 22237 . . . . . . . . . . . 12  |-  ( ( U  e.  CPreHil  /\  2  e.  ( Base `  (Scalar `  U ) )  /\  2  =/=  0 )  -> 
( 1  /  2
)  e.  ( Base `  (Scalar `  U )
) )
485, 44, 46, 47syl3anc 1292 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  /  2
)  e.  ( Base `  (Scalar `  U )
) )
49 eqid 2471 . . . . . . . . . . . . 13  |-  ( +g  `  U )  =  ( +g  `  U )
5049, 23lssvacl 18255 . . . . . . . . . . . 12  |-  ( ( ( U  e.  LMod  /\  Y  e.  ( LSubSp `  U ) )  /\  ( K  e.  Y  /\  L  e.  Y
) )  ->  ( K ( +g  `  U
) L )  e.  Y )
5135, 6, 26, 28, 50syl22anc 1293 . . . . . . . . . . 11  |-  ( ph  ->  ( K ( +g  `  U ) L )  e.  Y )
52 eqid 2471 . . . . . . . . . . . 12  |-  ( .s
`  U )  =  ( .s `  U
)
5338, 52, 39, 23lssvscl 18256 . . . . . . . . . . 11  |-  ( ( ( 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 )
5435, 6, 48, 51, 53syl22anc 1293 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  / 
2 ) ( .s
`  U ) ( K ( +g  `  U
) L ) )  e.  Y )
5525, 54sseldd 3419 . . . . . . . . 9  |-  ( ph  ->  ( ( 1  / 
2 ) ( .s
`  U ) ( K ( +g  `  U
) L ) )  e.  X )
562, 3lmodvsubcl 18211 . . . . . . . . 9  |-  ( ( 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 )
5735, 8, 55, 56syl3anc 1292 . . . . . . . 8  |-  ( ph  ->  ( A  .-  (
( 1  /  2
) ( .s `  U ) ( K ( +g  `  U
) L ) ) )  e.  X )
582, 4nmcl 21707 . . . . . . . 8  |-  ( ( 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 )
5917, 57, 58syl2anc 673 . . . . . . 7  |-  ( ph  ->  ( N `  ( A  .-  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) ) ) )  e.  RR )
6059resqcld 12480 . . . . . 6  |-  ( ph  ->  ( ( N `  ( A  .-  ( ( 1  /  2 ) ( .s `  U
) ( K ( +g  `  U ) L ) ) ) ) ^ 2 )  e.  RR )
61 remulcl 9642 . . . . . 6  |-  ( ( 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 )
621, 60, 61sylancr 676 . . . . 5  |-  ( ph  ->  ( 4  x.  (
( N `  ( A  .-  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) ) ) ) ^
2 ) )  e.  RR )
6362, 32readdcld 9688 . . . 4  |-  ( ph  ->  ( ( 4  x.  ( ( N `  ( A  .-  ( ( 1  /  2 ) ( .s `  U
) ( K ( +g  `  U ) L ) ) ) ) ^ 2 ) )  +  ( ( K D L ) ^ 2 ) )  e.  RR )
64 minveclem2OLD.1 . . . . . 6  |-  ( ph  ->  B  e.  RR )
6513, 64readdcld 9688 . . . . 5  |-  ( ph  ->  ( ( S ^
2 )  +  B
)  e.  RR )
66 remulcl 9642 . . . . 5  |-  ( ( 4  e.  RR  /\  ( ( S ^
2 )  +  B
)  e.  RR )  ->  ( 4  x.  ( ( S ^
2 )  +  B
) )  e.  RR )
671, 65, 66sylancr 676 . . . 4  |-  ( ph  ->  ( 4  x.  (
( S ^ 2 )  +  B ) )  e.  RR )
682, 3, 4, 5, 6, 7, 8, 9, 10minveclem1 22444 . . . . . . . . . 10  |-  ( ph  ->  ( R  C_  RR  /\  R  =/=  (/)  /\  A. w  e.  R  0  <_  w ) )
6968simp3d 1044 . . . . . . . . 9  |-  ( ph  ->  A. w  e.  R 
0  <_  w )
7068simp1d 1042 . . . . . . . . . 10  |-  ( ph  ->  R  C_  RR )
7168simp2d 1043 . . . . . . . . . 10  |-  ( ph  ->  R  =/=  (/) )
72 0re 9661 . . . . . . . . . . 11  |-  0  e.  RR
73 breq1 4398 . . . . . . . . . . . . 13  |-  ( x  =  0  ->  (
x  <_  w  <->  0  <_  w ) )
7473ralbidv 2829 . . . . . . . . . . . 12  |-  ( x  =  0  ->  ( A. w  e.  R  x  <_  w  <->  A. w  e.  R  0  <_  w ) )
7574rspcev 3136 . . . . . . . . . . 11  |-  ( ( 0  e.  RR  /\  A. w  e.  R  0  <_  w )  ->  E. x  e.  RR  A. w  e.  R  x  <_  w )
7672, 69, 75sylancr 676 . . . . . . . . . 10  |-  ( ph  ->  E. x  e.  RR  A. w  e.  R  x  <_  w )
7772a1i 11 . . . . . . . . . 10  |-  ( ph  ->  0  e.  RR )
78 infmrgelbOLD 10617 . . . . . . . . . 10  |-  ( ( ( R  C_  RR  /\  R  =/=  (/)  /\  E. x  e.  RR  A. w  e.  R  x  <_  w )  /\  0  e.  RR )  ->  (
0  <_  sup ( R ,  RR ,  `'  <  )  <->  A. w  e.  R  0  <_  w ) )
7970, 71, 76, 77, 78syl31anc 1295 . . . . . . . . 9  |-  ( ph  ->  ( 0  <_  sup ( R ,  RR ,  `'  <  )  <->  A. w  e.  R  0  <_  w ) )
8069, 79mpbird 240 . . . . . . . 8  |-  ( ph  ->  0  <_  sup ( R ,  RR ,  `'  <  ) )
8180, 11syl6breqr 4436 . . . . . . 7  |-  ( ph  ->  0  <_  S )
82 eqid 2471 . . . . . . . . . . . 12  |-  ( N `
 ( A  .-  ( ( 1  / 
2 ) ( .s
`  U ) ( K ( +g  `  U
) L ) ) ) )  =  ( N `  ( A 
.-  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) ) ) )
83 oveq2 6316 . . . . . . . . . . . . . . 15  |-  ( y  =  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) )  ->  ( A  .-  y )  =  ( A  .-  ( ( 1  /  2 ) ( .s `  U
) ( K ( +g  `  U ) L ) ) ) )
8483fveq2d 5883 . . . . . . . . . . . . . 14  |-  ( y  =  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) )  ->  ( N `  ( A  .-  y
) )  =  ( N `  ( A 
.-  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) ) ) ) )
8584eqeq2d 2481 . . . . . . . . . . . . 13  |-  ( y  =  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) )  ->  ( ( N `  ( A  .-  ( ( 1  / 
2 ) ( .s
`  U ) ( K ( +g  `  U
) L ) ) ) )  =  ( N `  ( A 
.-  y ) )  <-> 
( N `  ( A  .-  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) ) ) )  =  ( N `  ( A  .-  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) ) ) ) ) )
8685rspcev 3136 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) ) )
8754, 82, 86sylancl 675 . . . . . . . . . . 11  |-  ( ph  ->  E. y  e.  Y  ( N `  ( A 
.-  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) ) ) )  =  ( N `  ( A  .-  y ) ) )
88 eqid 2471 . . . . . . . . . . . 12  |-  ( y  e.  Y  |->  ( N `
 ( A  .-  y ) ) )  =  ( y  e.  Y  |->  ( N `  ( A  .-  y ) ) )
89 fvex 5889 . . . . . . . . . . . 12  |-  ( N `
 ( A  .-  y ) )  e. 
_V
9088, 89elrnmpti 5091 . . . . . . . . . . 11  |-  ( ( 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 ) ) )
9187, 90sylibr 217 . . . . . . . . . 10  |-  ( ph  ->  ( N `  ( A  .-  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) ) ) )  e. 
ran  ( y  e.  Y  |->  ( N `  ( A  .-  y ) ) ) )
9291, 10syl6eleqr 2560 . . . . . . . . 9  |-  ( ph  ->  ( N `  ( A  .-  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) ) ) )  e.  R )
93 infmrlbOLD 10619 . . . . . . . . 9  |-  ( ( 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 )  ->  sup ( R ,  RR ,  `'  <  )  <_  ( N `  ( A  .-  ( ( 1  /  2 ) ( .s `  U
) ( K ( +g  `  U ) L ) ) ) ) )
9470, 76, 92, 93syl3anc 1292 . . . . . . . 8  |-  ( ph  ->  sup ( R ,  RR ,  `'  <  )  <_  ( N `  ( A  .-  ( ( 1  /  2 ) ( .s `  U
) ( K ( +g  `  U ) L ) ) ) ) )
9511, 94syl5eqbr 4429 . . . . . . 7  |-  ( ph  ->  S  <_  ( N `  ( A  .-  (
( 1  /  2
) ( .s `  U ) ( K ( +g  `  U
) L ) ) ) ) )
96 le2sq2 12388 . . . . . . 7  |-  ( ( ( 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 ) )
9712, 81, 59, 95, 96syl22anc 1293 . . . . . 6  |-  ( ph  ->  ( S ^ 2 )  <_  ( ( N `  ( A  .-  ( ( 1  / 
2 ) ( .s
`  U ) ( K ( +g  `  U
) L ) ) ) ) ^ 2 ) )
98 4pos 10727 . . . . . . . . 9  |-  0  <  4
991, 98pm3.2i 462 . . . . . . . 8  |-  ( 4  e.  RR  /\  0  <  4 )
100 lemul2 10480 . . . . . . . 8  |-  ( ( ( 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 ) ) ) )
10199, 100mp3an3 1379 . . . . . . 7  |-  ( ( ( 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 ) ) ) )
10213, 60, 101syl2anc 673 . . . . . 6  |-  ( 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 ) ) ) )
10397, 102mpbid 215 . . . . 5  |-  ( ph  ->  ( 4  x.  ( S ^ 2 ) )  <_  ( 4  x.  ( ( N `  ( A  .-  ( ( 1  /  2 ) ( .s `  U
) ( K ( +g  `  U ) L ) ) ) ) ^ 2 ) ) )
10415, 62, 32, 103leadd1dd 10248 . . . 4  |-  ( 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 ) ) )
105 metcl 21425 . . . . . . . . . 10  |-  ( ( D  e.  ( Met `  X )  /\  A  e.  X  /\  K  e.  X )  ->  ( A D K )  e.  RR )
10622, 8, 27, 105syl3anc 1292 . . . . . . . . 9  |-  ( ph  ->  ( A D K )  e.  RR )
107106resqcld 12480 . . . . . . . 8  |-  ( ph  ->  ( ( A D K ) ^ 2 )  e.  RR )
108 metcl 21425 . . . . . . . . . 10  |-  ( ( D  e.  ( Met `  X )  /\  A  e.  X  /\  L  e.  X )  ->  ( A D L )  e.  RR )
10922, 8, 29, 108syl3anc 1292 . . . . . . . . 9  |-  ( ph  ->  ( A D L )  e.  RR )
110109resqcld 12480 . . . . . . . 8  |-  ( ph  ->  ( ( A D L ) ^ 2 )  e.  RR )
111 minveclem2OLD.5 . . . . . . . 8  |-  ( ph  ->  ( ( A D K ) ^ 2 )  <_  ( ( S ^ 2 )  +  B ) )
112 minveclem2OLD.6 . . . . . . . 8  |-  ( ph  ->  ( ( A D L ) ^ 2 )  <_  ( ( S ^ 2 )  +  B ) )
113107, 110, 65, 65, 111, 112le2addd 10253 . . . . . . 7  |-  ( ph  ->  ( ( ( A D K ) ^
2 )  +  ( ( A D L ) ^ 2 ) )  <_  ( (
( S ^ 2 )  +  B )  +  ( ( S ^ 2 )  +  B ) ) )
11465recnd 9687 . . . . . . . 8  |-  ( ph  ->  ( ( S ^
2 )  +  B
)  e.  CC )
1151142timesd 10878 . . . . . . 7  |-  ( ph  ->  ( 2  x.  (
( S ^ 2 )  +  B ) )  =  ( ( ( S ^ 2 )  +  B )  +  ( ( S ^ 2 )  +  B ) ) )
116113, 115breqtrrd 4422 . . . . . 6  |-  ( ph  ->  ( ( ( A D K ) ^
2 )  +  ( ( A D L ) ^ 2 ) )  <_  ( 2  x.  ( ( S ^ 2 )  +  B ) ) )
117107, 110readdcld 9688 . . . . . . 7  |-  ( ph  ->  ( ( ( A D K ) ^
2 )  +  ( ( A D L ) ^ 2 ) )  e.  RR )
118 2re 10701 . . . . . . . 8  |-  2  e.  RR
119 remulcl 9642 . . . . . . . 8  |-  ( ( 2  e.  RR  /\  ( ( S ^
2 )  +  B
)  e.  RR )  ->  ( 2  x.  ( ( S ^
2 )  +  B
) )  e.  RR )
120118, 65, 119sylancr 676 . . . . . . 7  |-  ( ph  ->  ( 2  x.  (
( S ^ 2 )  +  B ) )  e.  RR )
121 2pos 10723 . . . . . . . . 9  |-  0  <  2
122118, 121pm3.2i 462 . . . . . . . 8  |-  ( 2  e.  RR  /\  0  <  2 )
123 lemul2 10480 . . . . . . . 8  |-  ( ( ( ( ( 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 ) ) ) ) )
124122, 123mp3an3 1379 . . . . . . 7  |-  ( ( ( ( ( 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 ) ) ) ) )
125117, 120, 124syl2anc 673 . . . . . 6  |-  ( 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
) ) ) ) )
126116, 125mpbid 215 . . . . 5  |-  ( ph  ->  ( 2  x.  (
( ( A D K ) ^ 2 )  +  ( ( A D L ) ^ 2 ) ) )  <_  ( 2  x.  ( 2  x.  ( ( S ^
2 )  +  B
) ) ) )
1272, 3lmodvsubcl 18211 . . . . . . . 8  |-  ( ( U  e.  LMod  /\  A  e.  X  /\  K  e.  X )  ->  ( A  .-  K )  e.  X )
12835, 8, 27, 127syl3anc 1292 . . . . . . 7  |-  ( ph  ->  ( A  .-  K
)  e.  X )
1292, 3lmodvsubcl 18211 . . . . . . . 8  |-  ( ( U  e.  LMod  /\  A  e.  X  /\  L  e.  X )  ->  ( A  .-  L )  e.  X )
13035, 8, 29, 129syl3anc 1292 . . . . . . 7  |-  ( ph  ->  ( A  .-  L
)  e.  X )
1312, 49, 3, 4nmpar 22292 . . . . . . 7  |-  ( ( 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 ) ) ) )
1325, 128, 130, 131syl3anc 1292 . . . . . 6  |-  ( 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 10702 . . . . . . . . . 10  |-  2  e.  CC
13459recnd 9687 . . . . . . . . . 10  |-  ( ph  ->  ( N `  ( A  .-  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) ) ) )  e.  CC )
135 sqmul 12376 . . . . . . . . . 10  |-  ( ( 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 ) ) )
136133, 134, 135sylancr 676 . . . . . . . . 9  |-  ( 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 12409 . . . . . . . . . 10  |-  ( 2 ^ 2 )  =  4
138137oveq1i 6318 . . . . . . . . 9  |-  ( ( 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 ) )
139136, 138syl6eq 2521 . . . . . . . 8  |-  ( 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 ) ) )
1402, 4, 52, 38, 39cphnmvs 22246 . . . . . . . . . . . 12  |-  ( ( 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 ) ) ) ) ) )
1415, 44, 57, 140syl3anc 1292 . . . . . . . . . . 11  |-  ( 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 10722 . . . . . . . . . . . . 13  |-  0  <_  2
143 absid 13436 . . . . . . . . . . . . 13  |-  ( ( 2  e.  RR  /\  0  <_  2 )  -> 
( abs `  2
)  =  2 )
144118, 142, 143mp2an 686 . . . . . . . . . . . 12  |-  ( abs `  2 )  =  2
145144oveq1i 6318 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) ) )
146141, 145syl6eq 2521 . . . . . . . . . 10  |-  ( 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 ) ) ) ) ) )
1472, 52, 38, 39, 3, 35, 44, 8, 55lmodsubdi 18223 . . . . . . . . . . . 12  |-  ( 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 2471 . . . . . . . . . . . . . . . 16  |-  (.g `  U
)  =  (.g `  U
)
1492, 148, 49mulg2 16845 . . . . . . . . . . . . . . 15  |-  ( A  e.  X  ->  (
2 (.g `  U ) A )  =  ( A ( +g  `  U
) A ) )
1508, 149syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 2 (.g `  U
) A )  =  ( A ( +g  `  U ) A ) )
1512, 148, 52clmmulg 22202 . . . . . . . . . . . . . . 15  |-  ( ( U  e. CMod  /\  2  e.  ZZ  /\  A  e.  X )  ->  (
2 (.g `  U ) A )  =  ( 2 ( .s `  U
) A ) )
15237, 43, 8, 151syl3anc 1292 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 2 (.g `  U
) A )  =  ( 2 ( .s
`  U ) A ) )
153150, 152eqtr3d 2507 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A ( +g  `  U ) A )  =  ( 2 ( .s `  U ) A ) )
1542, 49lmodvacl 18183 . . . . . . . . . . . . . . . 16  |-  ( ( U  e.  LMod  /\  K  e.  X  /\  L  e.  X )  ->  ( K ( +g  `  U
) L )  e.  X )
15535, 27, 29, 154syl3anc 1292 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( K ( +g  `  U ) L )  e.  X )
1562, 52clmvs1 22198 . . . . . . . . . . . . . . 15  |-  ( ( U  e. CMod  /\  ( K ( +g  `  U
) L )  e.  X )  ->  (
1 ( .s `  U ) ( K ( +g  `  U
) L ) )  =  ( K ( +g  `  U ) L ) )
15737, 155, 156syl2anc 673 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1 ( .s
`  U ) ( K ( +g  `  U
) L ) )  =  ( K ( +g  `  U ) L ) )
158133, 45recidi 10360 . . . . . . . . . . . . . . . 16  |-  ( 2  x.  ( 1  / 
2 ) )  =  1
159158oveq1i 6318 . . . . . . . . . . . . . . 15  |-  ( ( 2  x.  ( 1  /  2 ) ) ( .s `  U
) ( K ( +g  `  U ) L ) )  =  ( 1 ( .s
`  U ) ( K ( +g  `  U
) L ) )
1602, 38, 52, 39clmvsass 22196 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) ) )
16137, 44, 48, 155, 160syl13anc 1294 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 2  x.  ( 1  /  2
) ) ( .s
`  U ) ( K ( +g  `  U
) L ) )  =  ( 2 ( .s `  U ) ( ( 1  / 
2 ) ( .s
`  U ) ( K ( +g  `  U
) L ) ) ) )
162159, 161syl5eqr 2519 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1 ( .s
`  U ) ( K ( +g  `  U
) L ) )  =  ( 2 ( .s `  U ) ( ( 1  / 
2 ) ( .s
`  U ) ( K ( +g  `  U
) L ) ) ) )
163157, 162eqtr3d 2507 . . . . . . . . . . . . 13  |-  ( ph  ->  ( K ( +g  `  U ) L )  =  ( 2 ( .s `  U ) ( ( 1  / 
2 ) ( .s
`  U ) ( K ( +g  `  U
) L ) ) ) )
164153, 163oveq12d 6326 . . . . . . . . . . . 12  |-  ( 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 18213 . . . . . . . . . . . . . 14  |-  ( U  e.  LMod  ->  U  e. 
Abel )
16635, 165syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  U  e.  Abel )
1672, 49, 3ablsub4 17533 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) )
168166, 8, 8, 27, 29, 167syl122anc 1301 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( A ( +g  `  U ) A )  .-  ( K ( +g  `  U
) L ) )  =  ( ( A 
.-  K ) ( +g  `  U ) ( A  .-  L
) ) )
169147, 164, 1683eqtr2d 2511 . . . . . . . . . . 11  |-  ( ph  ->  ( 2 ( .s
`  U ) ( A  .-  ( ( 1  /  2 ) ( .s `  U
) ( K ( +g  `  U ) L ) ) ) )  =  ( ( A  .-  K ) ( +g  `  U
) ( A  .-  L ) ) )
170169fveq2d 5883 . . . . . . . . . 10  |-  ( ph  ->  ( N `  (
2 ( .s `  U ) ( A 
.-  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) ) ) ) )  =  ( N `  ( ( A  .-  K ) ( +g  `  U ) ( A 
.-  L ) ) ) )
171146, 170eqtr3d 2507 . . . . . . . . 9  |-  ( ph  ->  ( 2  x.  ( N `  ( A  .-  ( ( 1  / 
2 ) ( .s
`  U ) ( K ( +g  `  U
) L ) ) ) ) )  =  ( N `  (
( A  .-  K
) ( +g  `  U
) ( A  .-  L ) ) ) )
172171oveq1d 6323 . . . . . . . 8  |-  ( ph  ->  ( ( 2  x.  ( N `  ( A  .-  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) ) ) ) ) ^ 2 )  =  ( ( N `  ( ( A  .-  K ) ( +g  `  U ) ( A 
.-  L ) ) ) ^ 2 ) )
173139, 172eqtr3d 2507 . . . . . . 7  |-  ( ph  ->  ( 4  x.  (
( N `  ( A  .-  ( ( 1  /  2 ) ( .s `  U ) ( K ( +g  `  U ) L ) ) ) ) ^
2 ) )  =  ( ( N `  ( ( A  .-  K ) ( +g  `  U ) ( A 
.-  L ) ) ) ^ 2 ) )
174 eqid 2471 . . . . . . . . . . 11  |-  ( dist `  U )  =  (
dist `  U )
1754, 2, 3, 174ngpdsr 21696 . . . . . . . . . 10  |-  ( ( U  e. NrmGrp  /\  K  e.  X  /\  L  e.  X )  ->  ( K ( dist `  U
) L )  =  ( N `  ( L  .-  K ) ) )
17617, 27, 29, 175syl3anc 1292 . . . . . . . . 9  |-  ( ph  ->  ( K ( dist `  U ) L )  =  ( N `  ( L  .-  K ) ) )
17720oveqi 6321 . . . . . . . . . 10  |-  ( K D L )  =  ( K ( (
dist `  U )  |`  ( X  X.  X
) ) L )
17827, 29ovresd 6456 . . . . . . . . . 10  |-  ( ph  ->  ( K ( (
dist `  U )  |`  ( X  X.  X
) ) L )  =  ( K (
dist `  U ) L ) )
179177, 178syl5eq 2517 . . . . . . . . 9  |-  ( ph  ->  ( K D L )  =  ( K ( dist `  U
) L ) )
1802, 3, 166, 8, 27, 29ablnnncan1 17543 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  .-  K )  .-  ( A  .-  L ) )  =  ( L  .-  K ) )
181180fveq2d 5883 . . . . . . . . 9  |-  ( ph  ->  ( N `  (
( A  .-  K
)  .-  ( A  .-  L ) ) )  =  ( N `  ( L  .-  K ) ) )
182176, 179, 1813eqtr4d 2515 . . . . . . . 8  |-  ( ph  ->  ( K D L )  =  ( N `
 ( ( A 
.-  K )  .-  ( A  .-  L ) ) ) )
183182oveq1d 6323 . . . . . . 7  |-  ( ph  ->  ( ( K D L ) ^ 2 )  =  ( ( N `  ( ( A  .-  K ) 
.-  ( A  .-  L ) ) ) ^ 2 ) )
184173, 183oveq12d 6326 . . . . . 6  |-  ( 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 ) ) )
18520oveqi 6321 . . . . . . . . . . 11  |-  ( A D K )  =  ( A ( (
dist `  U )  |`  ( X  X.  X
) ) K )
1868, 27ovresd 6456 . . . . . . . . . . 11  |-  ( ph  ->  ( A ( (
dist `  U )  |`  ( X  X.  X
) ) K )  =  ( A (
dist `  U ) K ) )
187185, 186syl5eq 2517 . . . . . . . . . 10  |-  ( ph  ->  ( A D K )  =  ( A ( dist `  U
) K ) )
1884, 2, 3, 174ngpds 21695 . . . . . . . . . . 11  |-  ( ( U  e. NrmGrp  /\  A  e.  X  /\  K  e.  X )  ->  ( A ( dist `  U
) K )  =  ( N `  ( A  .-  K ) ) )
18917, 8, 27, 188syl3anc 1292 . . . . . . . . . 10  |-  ( ph  ->  ( A ( dist `  U ) K )  =  ( N `  ( A  .-  K ) ) )
190187, 189eqtrd 2505 . . . . . . . . 9  |-  ( ph  ->  ( A D K )  =  ( N `
 ( A  .-  K ) ) )
191190oveq1d 6323 . . . . . . . 8  |-  ( ph  ->  ( ( A D K ) ^ 2 )  =  ( ( N `  ( A 
.-  K ) ) ^ 2 ) )
19220oveqi 6321 . . . . . . . . . . 11  |-  ( A D L )  =  ( A ( (
dist `  U )  |`  ( X  X.  X
) ) L )
1938, 29ovresd 6456 . . . . . . . . . . 11  |-  ( ph  ->  ( A ( (
dist `  U )  |`  ( X  X.  X
) ) L )  =  ( A (
dist `  U ) L ) )
194192, 193syl5eq 2517 . . . . . . . . . 10  |-  ( ph  ->  ( A D L )  =  ( A ( dist `  U
) L ) )
1954, 2, 3, 174ngpds 21695 . . . . . . . . . . 11  |-  ( ( U  e. NrmGrp  /\  A  e.  X  /\  L  e.  X )  ->  ( A ( dist `  U
) L )  =  ( N `  ( A  .-  L ) ) )
19617, 8, 29, 195syl3anc 1292 . . . . . . . . . 10  |-  ( ph  ->  ( A ( dist `  U ) L )  =  ( N `  ( A  .-  L ) ) )
197194, 196eqtrd 2505 . . . . . . . . 9  |-  ( ph  ->  ( A D L )  =  ( N `
 ( A  .-  L ) ) )
198197oveq1d 6323 . . . . . . . 8  |-  ( ph  ->  ( ( A D L ) ^ 2 )  =  ( ( N `  ( A 
.-  L ) ) ^ 2 ) )
199191, 198oveq12d 6326 . . . . . . 7  |-  ( ph  ->  ( ( ( A D K ) ^
2 )  +  ( ( A D L ) ^ 2 ) )  =  ( ( ( N `  ( A  .-  K ) ) ^ 2 )  +  ( ( N `  ( A  .-  L ) ) ^ 2 ) ) )
200199oveq2d 6324 . . . . . 6  |-  ( ph  ->  ( 2  x.  (
( ( A D K ) ^ 2 )  +  ( ( A D L ) ^ 2 ) ) )  =  ( 2  x.  ( ( ( N `  ( A 
.-  K ) ) ^ 2 )  +  ( ( N `  ( A  .-  L ) ) ^ 2 ) ) ) )
201132, 184, 2003eqtr4d 2515 . . . . 5  |-  ( 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 10782 . . . . . . 7  |-  ( 2  x.  2 )  =  4
203202oveq1i 6318 . . . . . 6  |-  ( ( 2  x.  2 )  x.  ( ( S ^ 2 )  +  B ) )  =  ( 4  x.  (
( S ^ 2 )  +  B ) )
204 2cnd 10704 . . . . . . 7  |-  ( ph  ->  2  e.  CC )
205204, 204, 114mulassd 9684 . . . . . 6  |-  ( ph  ->  ( ( 2  x.  2 )  x.  (
( S ^ 2 )  +  B ) )  =  ( 2  x.  ( 2  x.  ( ( S ^
2 )  +  B
) ) ) )
206203, 205syl5eqr 2519 . . . . 5  |-  ( ph  ->  ( 4  x.  (
( S ^ 2 )  +  B ) )  =  ( 2  x.  ( 2  x.  ( ( S ^
2 )  +  B
) ) ) )
207126, 201, 2063brtr4d 4426 . . . 4  |-  ( ph  ->  ( ( 4  x.  ( ( N `  ( A  .-  ( ( 1  /  2 ) ( .s `  U
) ( K ( +g  `  U ) L ) ) ) ) ^ 2 ) )  +  ( ( K D L ) ^ 2 ) )  <_  ( 4  x.  ( ( S ^
2 )  +  B
) ) )
20833, 63, 67, 104, 207letrd 9809 . . 3  |-  ( ph  ->  ( ( 4  x.  ( S ^ 2 ) )  +  ( ( K D L ) ^ 2 ) )  <_  ( 4  x.  ( ( S ^ 2 )  +  B ) ) )
209 4cn 10709 . . . . 5  |-  4  e.  CC
210209a1i 11 . . . 4  |-  ( ph  ->  4  e.  CC )
21113recnd 9687 . . . 4  |-  ( ph  ->  ( S ^ 2 )  e.  CC )
21264recnd 9687 . . . 4  |-  ( ph  ->  B  e.  CC )
213210, 211, 212adddid 9685 . . 3  |-  ( ph  ->  ( 4  x.  (
( S ^ 2 )  +  B ) )  =  ( ( 4  x.  ( S ^ 2 ) )  +  ( 4  x.  B ) ) )
214208, 213breqtrd 4420 . 2  |-  ( ph  ->  ( ( 4  x.  ( S ^ 2 ) )  +  ( ( K D L ) ^ 2 ) )  <_  ( (
4  x.  ( S ^ 2 ) )  +  ( 4  x.  B ) ) )
215 remulcl 9642 . . . 4  |-  ( ( 4  e.  RR  /\  B  e.  RR )  ->  ( 4  x.  B
)  e.  RR )
2161, 64, 215sylancr 676 . . 3  |-  ( ph  ->  ( 4  x.  B
)  e.  RR )
21732, 216, 15leadd2d 10229 . 2  |-  ( ph  ->  ( ( ( K D L ) ^
2 )  <_  (
4  x.  B )  <-> 
( ( 4  x.  ( S ^ 2 ) )  +  ( ( K D L ) ^ 2 ) )  <_  ( (
4  x.  ( S ^ 2 ) )  +  ( 4  x.  B ) ) ) )
218214, 217mpbird 240 1  |-  ( ph  ->  ( ( K D L ) ^ 2 )  <_  ( 4  x.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 376    = wceq 1452    e. wcel 1904    =/= wne 2641   A.wral 2756   E.wrex 2757    C_ wss 3390   (/)c0 3722   class class class wbr 4395    |-> cmpt 4454    X. cxp 4837   `'ccnv 4838   ran crn 4840    |` cres 4841   ` cfv 5589  (class class class)co 6308   supcsup 7972   CCcc 9555   RRcr 9556   0cc0 9557   1c1 9558    + caddc 9560    x. cmul 9562    < clt 9693    <_ cle 9694    / cdiv 10291   2c2 10681   4c4 10683   ZZcz 10961   ^cexp 12310   abscabs 13374   Basecbs 15199   ↾s cress 15200   +g cplusg 15268  Scalarcsca 15271   .scvsca 15272   distcds 15277   TopOpenctopn 15398   -gcsg 16749  .gcmg 16750   Abelcabl 17509   LModclmod 18169   LSubSpclss 18233   Metcme 19033   MetSpcmt 21411   normcnm 21669  NrmGrpcngp 21670  CModcclm 22171   CPreHilccph 22222  CMetSpccms 22378
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636  ax-mulf 9637
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-tpos 6991  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-map 7492  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-sup 7974  df-inf 7975  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-4 10692  df-5 10693  df-6 10694  df-7 10695  df-8 10696  df-9 10697  df-10 10698  df-n0 10894  df-z 10962  df-dec 11075  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-fz 11811  df-seq 12252  df-exp 12311  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-struct 15201  df-ndx 15202  df-slot 15203  df-base 15204  df-sets 15205  df-ress 15206  df-plusg 15281  df-mulr 15282  df-starv 15283  df-sca 15284  df-vsca 15285  df-ip 15286  df-tset 15287  df-ple 15288  df-ds 15290  df-unif 15291  df-0g 15418  df-topgen 15420  df-mgm 16566  df-sgrp 16605  df-mnd 16615  df-mhm 16660  df-grp 16751  df-minusg 16752  df-sbg 16753  df-mulg 16754  df-subg 16892  df-ghm 16959  df-cmn 17510  df-abl 17511  df-mgp 17802  df-ur 17814  df-ring 17860  df-cring 17861  df-oppr 17929  df-dvdsr 17947  df-unit 17948  df-invr 17978  df-dvr 17989  df-rnghom 18021  df-drng 18055  df-subrg 18084  df-staf 18151  df-srng 18152  df-lmod 18171  df-lss 18234  df-lmhm 18323  df-lvec 18404  df-sra 18473  df-rgmod 18474  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-cnfld 19048  df-phl 19270  df-top 19998  df-bases 19999  df-topon 20000  df-topsp 20001  df-xms 21413  df-ms 21414  df-nm 21675  df-ngp 21676  df-nlm 21679  df-clm 22172  df-cph 22224
This theorem is referenced by:  minveclem3OLD  22461  minveclem7OLD  22467
  Copyright terms: Public domain W3C validator