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

Theorem scvxcvx 20502
Description: A strictly convex function is convex. (Contributed by Mario Carneiro, 20-Jun-2015.)
Hypotheses
Ref Expression
scvxcvx.1  |-  ( ph  ->  D  C_  RR )
scvxcvx.2  |-  ( ph  ->  F : D --> RR )
scvxcvx.3  |-  ( (
ph  /\  ( a  e.  D  /\  b  e.  D ) )  -> 
( a [,] b
)  C_  D )
scvxcvx.4  |-  ( (
ph  /\  ( x  e.  D  /\  y  e.  D  /\  x  <  y )  /\  t  e.  ( 0 (,) 1
) )  ->  ( F `  ( (
t  x.  x )  +  ( ( 1  -  t )  x.  y ) ) )  <  ( ( t  x.  ( F `  x ) )  +  ( ( 1  -  t )  x.  ( F `  y )
) ) )
Assertion
Ref Expression
scvxcvx  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  <_  ( ( T  x.  ( F `  X ) )  +  ( ( 1  -  T )  x.  ( F `  Y )
) ) )
Distinct variable groups:    a, b,
t, x, y, D    ph, a, b, t, x, y    X, a, b, t, x, y    Y, a, b, t, x, y   
t, F, x, y   
t, T
Allowed substitution hints:    T( x, y, a, b)    F( a, b)

Proof of Theorem scvxcvx
StepHypRef Expression
1 scvxcvx.1 . . . . . . . . 9  |-  ( ph  ->  D  C_  RR )
21adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  D  C_  RR )
3 simpr1 962 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  X  e.  D )
42, 3sseldd 3267 . . . . . . 7  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  X  e.  RR )
54adantr 451 . . . . . 6  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  T  e.  ( 0 (,) 1
) )  ->  X  e.  RR )
6 simpr2 963 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  Y  e.  D )
72, 6sseldd 3267 . . . . . . 7  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  Y  e.  RR )
87adantr 451 . . . . . 6  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  T  e.  ( 0 (,) 1
) )  ->  Y  e.  RR )
95, 8lttri4d 9107 . . . . 5  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  T  e.  ( 0 (,) 1
) )  ->  ( X  <  Y  \/  X  =  Y  \/  Y  <  X ) )
10 simprl 732 . . . . . . . . 9  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  X  <  Y ) )  ->  T  e.  ( 0 (,) 1 ) )
113adantr 451 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  X  <  Y ) )  ->  X  e.  D )
126adantr 451 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  X  <  Y ) )  ->  Y  e.  D )
1311, 12jca 518 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  X  <  Y ) )  -> 
( X  e.  D  /\  Y  e.  D
) )
14 simprr 733 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  X  <  Y ) )  ->  X  <  Y )
15 simpll 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  X  <  Y ) )  ->  ph )
16 breq1 4128 . . . . . . . . . . . 12  |-  ( x  =  X  ->  (
x  <  y  <->  X  <  y ) )
17 oveq2 5989 . . . . . . . . . . . . . . . . 17  |-  ( x  =  X  ->  (
t  x.  x )  =  ( t  x.  X ) )
1817oveq1d 5996 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  (
( t  x.  x
)  +  ( ( 1  -  t )  x.  y ) )  =  ( ( t  x.  X )  +  ( ( 1  -  t )  x.  y
) ) )
1918fveq2d 5636 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  ( F `  ( (
t  x.  x )  +  ( ( 1  -  t )  x.  y ) ) )  =  ( F `  ( ( t  x.  X )  +  ( ( 1  -  t
)  x.  y ) ) ) )
20 fveq2 5632 . . . . . . . . . . . . . . . . 17  |-  ( x  =  X  ->  ( F `  x )  =  ( F `  X ) )
2120oveq2d 5997 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  (
t  x.  ( F `
 x ) )  =  ( t  x.  ( F `  X
) ) )
2221oveq1d 5996 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
( t  x.  ( F `  x )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) )  =  ( ( t  x.  ( F `  X ) )  +  ( ( 1  -  t )  x.  ( F `  y )
) ) )
2319, 22breq12d 4138 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
( F `  (
( t  x.  x
)  +  ( ( 1  -  t )  x.  y ) ) )  <  ( ( t  x.  ( F `
 x ) )  +  ( ( 1  -  t )  x.  ( F `  y
) ) )  <->  ( F `  ( ( t  x.  X )  +  ( ( 1  -  t
)  x.  y ) ) )  <  (
( t  x.  ( F `  X )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) ) ) )
2423ralbidv 2648 . . . . . . . . . . . . 13  |-  ( x  =  X  ->  ( A. t  e.  (
0 (,) 1 ) ( F `  (
( t  x.  x
)  +  ( ( 1  -  t )  x.  y ) ) )  <  ( ( t  x.  ( F `
 x ) )  +  ( ( 1  -  t )  x.  ( F `  y
) ) )  <->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  X )  +  ( ( 1  -  t
)  x.  y ) ) )  <  (
( t  x.  ( F `  X )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) ) ) )
2524imbi2d 307 . . . . . . . . . . . 12  |-  ( x  =  X  ->  (
( ph  ->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  x )  +  ( ( 1  -  t
)  x.  y ) ) )  <  (
( t  x.  ( F `  x )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) ) )  <->  ( ph  ->  A. t  e.  ( 0 (,) 1 ) ( F `  ( ( t  x.  X )  +  ( ( 1  -  t )  x.  y ) ) )  <  ( ( t  x.  ( F `  X ) )  +  ( ( 1  -  t )  x.  ( F `  y )
) ) ) ) )
2616, 25imbi12d 311 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
( x  <  y  ->  ( ph  ->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  x )  +  ( ( 1  -  t
)  x.  y ) ) )  <  (
( t  x.  ( F `  x )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) ) ) )  <->  ( X  <  y  ->  ( ph  ->  A. t  e.  ( 0 (,) 1 ) ( F `  (
( t  x.  X
)  +  ( ( 1  -  t )  x.  y ) ) )  <  ( ( t  x.  ( F `
 X ) )  +  ( ( 1  -  t )  x.  ( F `  y
) ) ) ) ) ) )
27 breq2 4129 . . . . . . . . . . . 12  |-  ( y  =  Y  ->  ( X  <  y  <->  X  <  Y ) )
28 oveq2 5989 . . . . . . . . . . . . . . . . 17  |-  ( y  =  Y  ->  (
( 1  -  t
)  x.  y )  =  ( ( 1  -  t )  x.  Y ) )
2928oveq2d 5997 . . . . . . . . . . . . . . . 16  |-  ( y  =  Y  ->  (
( t  x.  X
)  +  ( ( 1  -  t )  x.  y ) )  =  ( ( t  x.  X )  +  ( ( 1  -  t )  x.  Y
) ) )
3029fveq2d 5636 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  ( F `  ( (
t  x.  X )  +  ( ( 1  -  t )  x.  y ) ) )  =  ( F `  ( ( t  x.  X )  +  ( ( 1  -  t
)  x.  Y ) ) ) )
31 fveq2 5632 . . . . . . . . . . . . . . . . 17  |-  ( y  =  Y  ->  ( F `  y )  =  ( F `  Y ) )
3231oveq2d 5997 . . . . . . . . . . . . . . . 16  |-  ( y  =  Y  ->  (
( 1  -  t
)  x.  ( F `
 y ) )  =  ( ( 1  -  t )  x.  ( F `  Y
) ) )
3332oveq2d 5997 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  (
( t  x.  ( F `  X )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) )  =  ( ( t  x.  ( F `  X ) )  +  ( ( 1  -  t )  x.  ( F `  Y )
) ) )
3430, 33breq12d 4138 . . . . . . . . . . . . . 14  |-  ( y  =  Y  ->  (
( F `  (
( t  x.  X
)  +  ( ( 1  -  t )  x.  y ) ) )  <  ( ( t  x.  ( F `
 X ) )  +  ( ( 1  -  t )  x.  ( F `  y
) ) )  <->  ( F `  ( ( t  x.  X )  +  ( ( 1  -  t
)  x.  Y ) ) )  <  (
( t  x.  ( F `  X )
)  +  ( ( 1  -  t )  x.  ( F `  Y ) ) ) ) )
3534ralbidv 2648 . . . . . . . . . . . . 13  |-  ( y  =  Y  ->  ( A. t  e.  (
0 (,) 1 ) ( F `  (
( t  x.  X
)  +  ( ( 1  -  t )  x.  y ) ) )  <  ( ( t  x.  ( F `
 X ) )  +  ( ( 1  -  t )  x.  ( F `  y
) ) )  <->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  X )  +  ( ( 1  -  t
)  x.  Y ) ) )  <  (
( t  x.  ( F `  X )
)  +  ( ( 1  -  t )  x.  ( F `  Y ) ) ) ) )
3635imbi2d 307 . . . . . . . . . . . 12  |-  ( y  =  Y  ->  (
( ph  ->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  X )  +  ( ( 1  -  t
)  x.  y ) ) )  <  (
( t  x.  ( F `  X )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) ) )  <->  ( ph  ->  A. t  e.  ( 0 (,) 1 ) ( F `  ( ( t  x.  X )  +  ( ( 1  -  t )  x.  Y ) ) )  <  ( ( t  x.  ( F `  X ) )  +  ( ( 1  -  t )  x.  ( F `  Y )
) ) ) ) )
3727, 36imbi12d 311 . . . . . . . . . . 11  |-  ( y  =  Y  ->  (
( X  <  y  ->  ( ph  ->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  X )  +  ( ( 1  -  t
)  x.  y ) ) )  <  (
( t  x.  ( F `  X )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) ) ) )  <->  ( X  <  Y  ->  ( ph  ->  A. t  e.  ( 0 (,) 1 ) ( F `  (
( t  x.  X
)  +  ( ( 1  -  t )  x.  Y ) ) )  <  ( ( t  x.  ( F `
 X ) )  +  ( ( 1  -  t )  x.  ( F `  Y
) ) ) ) ) ) )
38 scvxcvx.4 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  D  /\  y  e.  D  /\  x  <  y )  /\  t  e.  ( 0 (,) 1
) )  ->  ( F `  ( (
t  x.  x )  +  ( ( 1  -  t )  x.  y ) ) )  <  ( ( t  x.  ( F `  x ) )  +  ( ( 1  -  t )  x.  ( F `  y )
) ) )
39383expia 1154 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  D  /\  y  e.  D  /\  x  <  y ) )  -> 
( t  e.  ( 0 (,) 1 )  ->  ( F `  ( ( t  x.  x )  +  ( ( 1  -  t
)  x.  y ) ) )  <  (
( t  x.  ( F `  x )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) ) ) )
4039ralrimiv 2710 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  D  /\  y  e.  D  /\  x  <  y ) )  ->  A. t  e.  (
0 (,) 1 ) ( F `  (
( t  x.  x
)  +  ( ( 1  -  t )  x.  y ) ) )  <  ( ( t  x.  ( F `
 x ) )  +  ( ( 1  -  t )  x.  ( F `  y
) ) ) )
4140expcom 424 . . . . . . . . . . . 12  |-  ( ( x  e.  D  /\  y  e.  D  /\  x  <  y )  -> 
( ph  ->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  x )  +  ( ( 1  -  t
)  x.  y ) ) )  <  (
( t  x.  ( F `  x )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) ) ) )
42413expia 1154 . . . . . . . . . . 11  |-  ( ( x  e.  D  /\  y  e.  D )  ->  ( x  <  y  ->  ( ph  ->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  x )  +  ( ( 1  -  t
)  x.  y ) ) )  <  (
( t  x.  ( F `  x )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) ) ) ) )
4326, 37, 42vtocl2ga 2936 . . . . . . . . . 10  |-  ( ( X  e.  D  /\  Y  e.  D )  ->  ( X  <  Y  ->  ( ph  ->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  X )  +  ( ( 1  -  t
)  x.  Y ) ) )  <  (
( t  x.  ( F `  X )
)  +  ( ( 1  -  t )  x.  ( F `  Y ) ) ) ) ) )
4413, 14, 15, 43syl3c 57 . . . . . . . . 9  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  X  <  Y ) )  ->  A. t  e.  (
0 (,) 1 ) ( F `  (
( t  x.  X
)  +  ( ( 1  -  t )  x.  Y ) ) )  <  ( ( t  x.  ( F `
 X ) )  +  ( ( 1  -  t )  x.  ( F `  Y
) ) ) )
45 oveq1 5988 . . . . . . . . . . . . 13  |-  ( t  =  T  ->  (
t  x.  X )  =  ( T  x.  X ) )
46 oveq2 5989 . . . . . . . . . . . . . 14  |-  ( t  =  T  ->  (
1  -  t )  =  ( 1  -  T ) )
4746oveq1d 5996 . . . . . . . . . . . . 13  |-  ( t  =  T  ->  (
( 1  -  t
)  x.  Y )  =  ( ( 1  -  T )  x.  Y ) )
4845, 47oveq12d 5999 . . . . . . . . . . . 12  |-  ( t  =  T  ->  (
( t  x.  X
)  +  ( ( 1  -  t )  x.  Y ) )  =  ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y
) ) )
4948fveq2d 5636 . . . . . . . . . . 11  |-  ( t  =  T  ->  ( F `  ( (
t  x.  X )  +  ( ( 1  -  t )  x.  Y ) ) )  =  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) ) )
50 oveq1 5988 . . . . . . . . . . . 12  |-  ( t  =  T  ->  (
t  x.  ( F `
 X ) )  =  ( T  x.  ( F `  X ) ) )
5146oveq1d 5996 . . . . . . . . . . . 12  |-  ( t  =  T  ->  (
( 1  -  t
)  x.  ( F `
 Y ) )  =  ( ( 1  -  T )  x.  ( F `  Y
) ) )
5250, 51oveq12d 5999 . . . . . . . . . . 11  |-  ( t  =  T  ->  (
( t  x.  ( F `  X )
)  +  ( ( 1  -  t )  x.  ( F `  Y ) ) )  =  ( ( T  x.  ( F `  X ) )  +  ( ( 1  -  T )  x.  ( F `  Y )
) ) )
5349, 52breq12d 4138 . . . . . . . . . 10  |-  ( t  =  T  ->  (
( F `  (
( t  x.  X
)  +  ( ( 1  -  t )  x.  Y ) ) )  <  ( ( t  x.  ( F `
 X ) )  +  ( ( 1  -  t )  x.  ( F `  Y
) ) )  <->  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  <  (
( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) ) ) )
5453rspcv 2965 . . . . . . . . 9  |-  ( T  e.  ( 0 (,) 1 )  ->  ( A. t  e.  (
0 (,) 1 ) ( F `  (
( t  x.  X
)  +  ( ( 1  -  t )  x.  Y ) ) )  <  ( ( t  x.  ( F `
 X ) )  +  ( ( 1  -  t )  x.  ( F `  Y
) ) )  -> 
( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  <  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) ) ) )
5510, 44, 54sylc 56 . . . . . . . 8  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  X  <  Y ) )  -> 
( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  <  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) ) )
5655orcd 381 . . . . . . 7  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  X  <  Y ) )  -> 
( ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  <  (
( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  \/  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  =  ( ( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) ) ) )
5756expr 598 . . . . . 6  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  T  e.  ( 0 (,) 1
) )  ->  ( X  <  Y  ->  (
( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  <  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) )  \/  ( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) ) ) ) )
58 0re 8985 . . . . . . . . . . . . . . . . 17  |-  0  e.  RR
59 1re 8984 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR
60 iccssre 10884 . . . . . . . . . . . . . . . . 17  |-  ( ( 0  e.  RR  /\  1  e.  RR )  ->  ( 0 [,] 1
)  C_  RR )
6158, 59, 60mp2an 653 . . . . . . . . . . . . . . . 16  |-  ( 0 [,] 1 )  C_  RR
62 simpr3 964 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  T  e.  ( 0 [,] 1 ) )
6361, 62sseldi 3264 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  T  e.  RR )
6463recnd 9008 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  T  e.  CC )
65 ax-1cn 8942 . . . . . . . . . . . . . 14  |-  1  e.  CC
66 pncan3 9206 . . . . . . . . . . . . . 14  |-  ( ( T  e.  CC  /\  1  e.  CC )  ->  ( T  +  ( 1  -  T ) )  =  1 )
6764, 65, 66sylancl 643 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( T  +  ( 1  -  T ) )  =  1 )
6867oveq1d 5996 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( T  +  ( 1  -  T
) )  x.  Y
)  =  ( 1  x.  Y ) )
69 subcl 9198 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  CC  /\  T  e.  CC )  ->  ( 1  -  T
)  e.  CC )
7065, 64, 69sylancr 644 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 1  -  T
)  e.  CC )
717recnd 9008 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  Y  e.  CC )
7264, 70, 71adddird 9007 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( T  +  ( 1  -  T
) )  x.  Y
)  =  ( ( T  x.  Y )  +  ( ( 1  -  T )  x.  Y ) ) )
7371mulid2d 9000 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 1  x.  Y
)  =  Y )
7468, 72, 733eqtr3d 2406 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( T  x.  Y )  +  ( ( 1  -  T
)  x.  Y ) )  =  Y )
7574fveq2d 5636 . . . . . . . . . 10  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  (
( T  x.  Y
)  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( F `
 Y ) )
7667oveq1d 5996 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( T  +  ( 1  -  T
) )  x.  ( F `  Y )
)  =  ( 1  x.  ( F `  Y ) ) )
77 scvxcvx.2 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F : D --> RR )
7877adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  F : D --> RR )
79 ffvelrn 5770 . . . . . . . . . . . . . 14  |-  ( ( F : D --> RR  /\  Y  e.  D )  ->  ( F `  Y
)  e.  RR )
8078, 6, 79syl2anc 642 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  Y
)  e.  RR )
8180recnd 9008 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  Y
)  e.  CC )
8264, 70, 81adddird 9007 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( T  +  ( 1  -  T
) )  x.  ( F `  Y )
)  =  ( ( T  x.  ( F `
 Y ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) ) )
8381mulid2d 9000 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 1  x.  ( F `  Y )
)  =  ( F `
 Y ) )
8476, 82, 833eqtr3d 2406 . . . . . . . . . 10  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( T  x.  ( F `  Y ) )  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  =  ( F `  Y ) )
8575, 84eqtr4d 2401 . . . . . . . . 9  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  (
( T  x.  Y
)  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( ( T  x.  ( F `
 Y ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) ) )
8685adantr 451 . . . . . . . 8  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  T  e.  ( 0 (,) 1
) )  ->  ( F `  ( ( T  x.  Y )  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( ( T  x.  ( F `  Y ) )  +  ( ( 1  -  T )  x.  ( F `  Y )
) ) )
87 oveq2 5989 . . . . . . . . . . 11  |-  ( X  =  Y  ->  ( T  x.  X )  =  ( T  x.  Y ) )
8887oveq1d 5996 . . . . . . . . . 10  |-  ( X  =  Y  ->  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) )  =  ( ( T  x.  Y )  +  ( ( 1  -  T )  x.  Y
) ) )
8988fveq2d 5636 . . . . . . . . 9  |-  ( X  =  Y  ->  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( F `  ( ( T  x.  Y )  +  ( ( 1  -  T
)  x.  Y ) ) ) )
90 fveq2 5632 . . . . . . . . . . 11  |-  ( X  =  Y  ->  ( F `  X )  =  ( F `  Y ) )
9190oveq2d 5997 . . . . . . . . . 10  |-  ( X  =  Y  ->  ( T  x.  ( F `  X ) )  =  ( T  x.  ( F `  Y )
) )
9291oveq1d 5996 . . . . . . . . 9  |-  ( X  =  Y  ->  (
( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  =  ( ( T  x.  ( F `  Y ) )  +  ( ( 1  -  T )  x.  ( F `  Y )
) ) )
9389, 92eqeq12d 2380 . . . . . . . 8  |-  ( X  =  Y  ->  (
( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) )  <->  ( F `  ( ( T  x.  Y )  +  ( ( 1  -  T
)  x.  Y ) ) )  =  ( ( T  x.  ( F `  Y )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) ) ) )
9486, 93syl5ibrcom 213 . . . . . . 7  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  T  e.  ( 0 (,) 1
) )  ->  ( X  =  Y  ->  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( ( T  x.  ( F `  X ) )  +  ( ( 1  -  T )  x.  ( F `  Y )
) ) ) )
95 olc 373 . . . . . . 7  |-  ( ( F `  ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( ( T  x.  ( F `  X ) )  +  ( ( 1  -  T )  x.  ( F `  Y )
) )  ->  (
( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  <  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) )  \/  ( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) ) ) )
9694, 95syl6 29 . . . . . 6  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  T  e.  ( 0 (,) 1
) )  ->  ( X  =  Y  ->  ( ( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  <  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) )  \/  ( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) ) ) ) )
97 elioore 10839 . . . . . . . . . . . . 13  |-  ( T  e.  ( 0 (,) 1 )  ->  T  e.  RR )
98 resubcl 9258 . . . . . . . . . . . . 13  |-  ( ( 1  e.  RR  /\  T  e.  RR )  ->  ( 1  -  T
)  e.  RR )
9959, 97, 98sylancr 644 . . . . . . . . . . . 12  |-  ( T  e.  ( 0 (,) 1 )  ->  (
1  -  T )  e.  RR )
100 eliooord 10863 . . . . . . . . . . . . . 14  |-  ( T  e.  ( 0 (,) 1 )  ->  (
0  <  T  /\  T  <  1 ) )
101100simprd 449 . . . . . . . . . . . . 13  |-  ( T  e.  ( 0 (,) 1 )  ->  T  <  1 )
102 posdif 9414 . . . . . . . . . . . . . 14  |-  ( ( T  e.  RR  /\  1  e.  RR )  ->  ( T  <  1  <->  0  <  ( 1  -  T ) ) )
10397, 59, 102sylancl 643 . . . . . . . . . . . . 13  |-  ( T  e.  ( 0 (,) 1 )  ->  ( T  <  1  <->  0  <  ( 1  -  T ) ) )
104101, 103mpbid 201 . . . . . . . . . . . 12  |-  ( T  e.  ( 0 (,) 1 )  ->  0  <  ( 1  -  T
) )
105100simpld 445 . . . . . . . . . . . . 13  |-  ( T  e.  ( 0 (,) 1 )  ->  0  <  T )
106 ltsubpos 9413 . . . . . . . . . . . . . 14  |-  ( ( T  e.  RR  /\  1  e.  RR )  ->  ( 0  <  T  <->  ( 1  -  T )  <  1 ) )
10797, 59, 106sylancl 643 . . . . . . . . . . . . 13  |-  ( T  e.  ( 0 (,) 1 )  ->  (
0  <  T  <->  ( 1  -  T )  <  1 ) )
108105, 107mpbid 201 . . . . . . . . . . . 12  |-  ( T  e.  ( 0 (,) 1 )  ->  (
1  -  T )  <  1 )
109 0xr 9025 . . . . . . . . . . . . 13  |-  0  e.  RR*
110 ressxr 9023 . . . . . . . . . . . . . 14  |-  RR  C_  RR*
111110, 59sselii 3263 . . . . . . . . . . . . 13  |-  1  e.  RR*
112 elioo2 10850 . . . . . . . . . . . . 13  |-  ( ( 0  e.  RR*  /\  1  e.  RR* )  ->  (
( 1  -  T
)  e.  ( 0 (,) 1 )  <->  ( (
1  -  T )  e.  RR  /\  0  <  ( 1  -  T
)  /\  ( 1  -  T )  <  1 ) ) )
113109, 111, 112mp2an 653 . . . . . . . . . . . 12  |-  ( ( 1  -  T )  e.  ( 0 (,) 1 )  <->  ( (
1  -  T )  e.  RR  /\  0  <  ( 1  -  T
)  /\  ( 1  -  T )  <  1 ) )
11499, 104, 108, 113syl3anbrc 1137 . . . . . . . . . . 11  |-  ( T  e.  ( 0 (,) 1 )  ->  (
1  -  T )  e.  ( 0 (,) 1 ) )
115114ad2antrl 708 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  Y  <  X ) )  -> 
( 1  -  T
)  e.  ( 0 (,) 1 ) )
1166adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  Y  <  X ) )  ->  Y  e.  D )
1173adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  Y  <  X ) )  ->  X  e.  D )
118116, 117jca 518 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  Y  <  X ) )  -> 
( Y  e.  D  /\  X  e.  D
) )
119 simprr 733 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  Y  <  X ) )  ->  Y  <  X )
120 simpll 730 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  Y  <  X ) )  ->  ph )
121 breq1 4128 . . . . . . . . . . . . 13  |-  ( x  =  Y  ->  (
x  <  y  <->  Y  <  y ) )
122 oveq2 5989 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  Y  ->  (
t  x.  x )  =  ( t  x.  Y ) )
123122oveq1d 5996 . . . . . . . . . . . . . . . . 17  |-  ( x  =  Y  ->  (
( t  x.  x
)  +  ( ( 1  -  t )  x.  y ) )  =  ( ( t  x.  Y )  +  ( ( 1  -  t )  x.  y
) ) )
124123fveq2d 5636 . . . . . . . . . . . . . . . 16  |-  ( x  =  Y  ->  ( F `  ( (
t  x.  x )  +  ( ( 1  -  t )  x.  y ) ) )  =  ( F `  ( ( t  x.  Y )  +  ( ( 1  -  t
)  x.  y ) ) ) )
125 fveq2 5632 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  Y  ->  ( F `  x )  =  ( F `  Y ) )
126125oveq2d 5997 . . . . . . . . . . . . . . . . 17  |-  ( x  =  Y  ->  (
t  x.  ( F `
 x ) )  =  ( t  x.  ( F `  Y
) ) )
127126oveq1d 5996 . . . . . . . . . . . . . . . 16  |-  ( x  =  Y  ->  (
( t  x.  ( F `  x )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) )  =  ( ( t  x.  ( F `  Y ) )  +  ( ( 1  -  t )  x.  ( F `  y )
) ) )
128124, 127breq12d 4138 . . . . . . . . . . . . . . 15  |-  ( x  =  Y  ->  (
( F `  (
( t  x.  x
)  +  ( ( 1  -  t )  x.  y ) ) )  <  ( ( t  x.  ( F `
 x ) )  +  ( ( 1  -  t )  x.  ( F `  y
) ) )  <->  ( F `  ( ( t  x.  Y )  +  ( ( 1  -  t
)  x.  y ) ) )  <  (
( t  x.  ( F `  Y )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) ) ) )
129128ralbidv 2648 . . . . . . . . . . . . . 14  |-  ( x  =  Y  ->  ( A. t  e.  (
0 (,) 1 ) ( F `  (
( t  x.  x
)  +  ( ( 1  -  t )  x.  y ) ) )  <  ( ( t  x.  ( F `
 x ) )  +  ( ( 1  -  t )  x.  ( F `  y
) ) )  <->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  Y )  +  ( ( 1  -  t
)  x.  y ) ) )  <  (
( t  x.  ( F `  Y )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) ) ) )
130129imbi2d 307 . . . . . . . . . . . . 13  |-  ( x  =  Y  ->  (
( ph  ->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  x )  +  ( ( 1  -  t
)  x.  y ) ) )  <  (
( t  x.  ( F `  x )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) ) )  <->  ( ph  ->  A. t  e.  ( 0 (,) 1 ) ( F `  ( ( t  x.  Y )  +  ( ( 1  -  t )  x.  y ) ) )  <  ( ( t  x.  ( F `  Y ) )  +  ( ( 1  -  t )  x.  ( F `  y )
) ) ) ) )
131121, 130imbi12d 311 . . . . . . . . . . . 12  |-  ( x  =  Y  ->  (
( x  <  y  ->  ( ph  ->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  x )  +  ( ( 1  -  t
)  x.  y ) ) )  <  (
( t  x.  ( F `  x )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) ) ) )  <->  ( Y  <  y  ->  ( ph  ->  A. t  e.  ( 0 (,) 1 ) ( F `  (
( t  x.  Y
)  +  ( ( 1  -  t )  x.  y ) ) )  <  ( ( t  x.  ( F `
 Y ) )  +  ( ( 1  -  t )  x.  ( F `  y
) ) ) ) ) ) )
132 breq2 4129 . . . . . . . . . . . . 13  |-  ( y  =  X  ->  ( Y  <  y  <->  Y  <  X ) )
133 oveq2 5989 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  X  ->  (
( 1  -  t
)  x.  y )  =  ( ( 1  -  t )  x.  X ) )
134133oveq2d 5997 . . . . . . . . . . . . . . . . 17  |-  ( y  =  X  ->  (
( t  x.  Y
)  +  ( ( 1  -  t )  x.  y ) )  =  ( ( t  x.  Y )  +  ( ( 1  -  t )  x.  X
) ) )
135134fveq2d 5636 . . . . . . . . . . . . . . . 16  |-  ( y  =  X  ->  ( F `  ( (
t  x.  Y )  +  ( ( 1  -  t )  x.  y ) ) )  =  ( F `  ( ( t  x.  Y )  +  ( ( 1  -  t
)  x.  X ) ) ) )
136 fveq2 5632 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  X  ->  ( F `  y )  =  ( F `  X ) )
137136oveq2d 5997 . . . . . . . . . . . . . . . . 17  |-  ( y  =  X  ->  (
( 1  -  t
)  x.  ( F `
 y ) )  =  ( ( 1  -  t )  x.  ( F `  X
) ) )
138137oveq2d 5997 . . . . . . . . . . . . . . . 16  |-  ( y  =  X  ->  (
( t  x.  ( F `  Y )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) )  =  ( ( t  x.  ( F `  Y ) )  +  ( ( 1  -  t )  x.  ( F `  X )
) ) )
139135, 138breq12d 4138 . . . . . . . . . . . . . . 15  |-  ( y  =  X  ->  (
( F `  (
( t  x.  Y
)  +  ( ( 1  -  t )  x.  y ) ) )  <  ( ( t  x.  ( F `
 Y ) )  +  ( ( 1  -  t )  x.  ( F `  y
) ) )  <->  ( F `  ( ( t  x.  Y )  +  ( ( 1  -  t
)  x.  X ) ) )  <  (
( t  x.  ( F `  Y )
)  +  ( ( 1  -  t )  x.  ( F `  X ) ) ) ) )
140139ralbidv 2648 . . . . . . . . . . . . . 14  |-  ( y  =  X  ->  ( A. t  e.  (
0 (,) 1 ) ( F `  (
( t  x.  Y
)  +  ( ( 1  -  t )  x.  y ) ) )  <  ( ( t  x.  ( F `
 Y ) )  +  ( ( 1  -  t )  x.  ( F `  y
) ) )  <->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  Y )  +  ( ( 1  -  t
)  x.  X ) ) )  <  (
( t  x.  ( F `  Y )
)  +  ( ( 1  -  t )  x.  ( F `  X ) ) ) ) )
141140imbi2d 307 . . . . . . . . . . . . 13  |-  ( y  =  X  ->  (
( ph  ->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  Y )  +  ( ( 1  -  t
)  x.  y ) ) )  <  (
( t  x.  ( F `  Y )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) ) )  <->  ( ph  ->  A. t  e.  ( 0 (,) 1 ) ( F `  ( ( t  x.  Y )  +  ( ( 1  -  t )  x.  X ) ) )  <  ( ( t  x.  ( F `  Y ) )  +  ( ( 1  -  t )  x.  ( F `  X )
) ) ) ) )
142132, 141imbi12d 311 . . . . . . . . . . . 12  |-  ( y  =  X  ->  (
( Y  <  y  ->  ( ph  ->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  Y )  +  ( ( 1  -  t
)  x.  y ) ) )  <  (
( t  x.  ( F `  Y )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) ) ) )  <->  ( Y  <  X  ->  ( ph  ->  A. t  e.  ( 0 (,) 1 ) ( F `  (
( t  x.  Y
)  +  ( ( 1  -  t )  x.  X ) ) )  <  ( ( t  x.  ( F `
 Y ) )  +  ( ( 1  -  t )  x.  ( F `  X
) ) ) ) ) ) )
143131, 142, 42vtocl2ga 2936 . . . . . . . . . . 11  |-  ( ( Y  e.  D  /\  X  e.  D )  ->  ( Y  <  X  ->  ( ph  ->  A. t  e.  ( 0 (,) 1
) ( F `  ( ( t  x.  Y )  +  ( ( 1  -  t
)  x.  X ) ) )  <  (
( t  x.  ( F `  Y )
)  +  ( ( 1  -  t )  x.  ( F `  X ) ) ) ) ) )
144118, 119, 120, 143syl3c 57 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  Y  <  X ) )  ->  A. t  e.  (
0 (,) 1 ) ( F `  (
( t  x.  Y
)  +  ( ( 1  -  t )  x.  X ) ) )  <  ( ( t  x.  ( F `
 Y ) )  +  ( ( 1  -  t )  x.  ( F `  X
) ) ) )
145 oveq1 5988 . . . . . . . . . . . . . 14  |-  ( t  =  ( 1  -  T )  ->  (
t  x.  Y )  =  ( ( 1  -  T )  x.  Y ) )
146 oveq2 5989 . . . . . . . . . . . . . . 15  |-  ( t  =  ( 1  -  T )  ->  (
1  -  t )  =  ( 1  -  ( 1  -  T
) ) )
147146oveq1d 5996 . . . . . . . . . . . . . 14  |-  ( t  =  ( 1  -  T )  ->  (
( 1  -  t
)  x.  X )  =  ( ( 1  -  ( 1  -  T ) )  x.  X ) )
148145, 147oveq12d 5999 . . . . . . . . . . . . 13  |-  ( t  =  ( 1  -  T )  ->  (
( t  x.  Y
)  +  ( ( 1  -  t )  x.  X ) )  =  ( ( ( 1  -  T )  x.  Y )  +  ( ( 1  -  ( 1  -  T
) )  x.  X
) ) )
149148fveq2d 5636 . . . . . . . . . . . 12  |-  ( t  =  ( 1  -  T )  ->  ( F `  ( (
t  x.  Y )  +  ( ( 1  -  t )  x.  X ) ) )  =  ( F `  ( ( ( 1  -  T )  x.  Y )  +  ( ( 1  -  (
1  -  T ) )  x.  X ) ) ) )
150 oveq1 5988 . . . . . . . . . . . . 13  |-  ( t  =  ( 1  -  T )  ->  (
t  x.  ( F `
 Y ) )  =  ( ( 1  -  T )  x.  ( F `  Y
) ) )
151146oveq1d 5996 . . . . . . . . . . . . 13  |-  ( t  =  ( 1  -  T )  ->  (
( 1  -  t
)  x.  ( F `
 X ) )  =  ( ( 1  -  ( 1  -  T ) )  x.  ( F `  X
) ) )
152150, 151oveq12d 5999 . . . . . . . . . . . 12  |-  ( t  =  ( 1  -  T )  ->  (
( t  x.  ( F `  Y )
)  +  ( ( 1  -  t )  x.  ( F `  X ) ) )  =  ( ( ( 1  -  T )  x.  ( F `  Y ) )  +  ( ( 1  -  ( 1  -  T
) )  x.  ( F `  X )
) ) )
153149, 152breq12d 4138 . . . . . . . . . . 11  |-  ( t  =  ( 1  -  T )  ->  (
( F `  (
( t  x.  Y
)  +  ( ( 1  -  t )  x.  X ) ) )  <  ( ( t  x.  ( F `
 Y ) )  +  ( ( 1  -  t )  x.  ( F `  X
) ) )  <->  ( F `  ( ( ( 1  -  T )  x.  Y )  +  ( ( 1  -  (
1  -  T ) )  x.  X ) ) )  <  (
( ( 1  -  T )  x.  ( F `  Y )
)  +  ( ( 1  -  ( 1  -  T ) )  x.  ( F `  X ) ) ) ) )
154153rspcv 2965 . . . . . . . . . 10  |-  ( ( 1  -  T )  e.  ( 0 (,) 1 )  ->  ( A. t  e.  (
0 (,) 1 ) ( F `  (
( t  x.  Y
)  +  ( ( 1  -  t )  x.  X ) ) )  <  ( ( t  x.  ( F `
 Y ) )  +  ( ( 1  -  t )  x.  ( F `  X
) ) )  -> 
( F `  (
( ( 1  -  T )  x.  Y
)  +  ( ( 1  -  ( 1  -  T ) )  x.  X ) ) )  <  ( ( ( 1  -  T
)  x.  ( F `
 Y ) )  +  ( ( 1  -  ( 1  -  T ) )  x.  ( F `  X
) ) ) ) )
155115, 144, 154sylc 56 . . . . . . . . 9  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  Y  <  X ) )  -> 
( F `  (
( ( 1  -  T )  x.  Y
)  +  ( ( 1  -  ( 1  -  T ) )  x.  X ) ) )  <  ( ( ( 1  -  T
)  x.  ( F `
 Y ) )  +  ( ( 1  -  ( 1  -  T ) )  x.  ( F `  X
) ) ) )
156 nncan 9223 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  CC  /\  T  e.  CC )  ->  ( 1  -  (
1  -  T ) )  =  T )
15765, 64, 156sylancr 644 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 1  -  (
1  -  T ) )  =  T )
158157oveq1d 5996 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  -  ( 1  -  T
) )  x.  X
)  =  ( T  x.  X ) )
159158oveq2d 5997 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( ( 1  -  T )  x.  Y )  +  ( ( 1  -  (
1  -  T ) )  x.  X ) )  =  ( ( ( 1  -  T
)  x.  Y )  +  ( T  x.  X ) ) )
16059, 63, 98sylancr 644 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 1  -  T
)  e.  RR )
161160, 7remulcld 9010 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  -  T )  x.  Y
)  e.  RR )
162161recnd 9008 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  -  T )  x.  Y
)  e.  CC )
16363, 4remulcld 9010 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( T  x.  X
)  e.  RR )
164163recnd 9008 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( T  x.  X
)  e.  CC )
165162, 164addcomd 9161 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( ( 1  -  T )  x.  Y )  +  ( T  x.  X ) )  =  ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y ) ) )
166159, 165eqtrd 2398 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( ( 1  -  T )  x.  Y )  +  ( ( 1  -  (
1  -  T ) )  x.  X ) )  =  ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y ) ) )
167166adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  Y  <  X ) )  -> 
( ( ( 1  -  T )  x.  Y )  +  ( ( 1  -  (
1  -  T ) )  x.  X ) )  =  ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y ) ) )
168167fveq2d 5636 . . . . . . . . 9  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  Y  <  X ) )  -> 
( F `  (
( ( 1  -  T )  x.  Y
)  +  ( ( 1  -  ( 1  -  T ) )  x.  X ) ) )  =  ( F `
 ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y
) ) ) )
169157oveq1d 5996 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  -  ( 1  -  T
) )  x.  ( F `  X )
)  =  ( T  x.  ( F `  X ) ) )
170169oveq2d 5997 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( ( 1  -  T )  x.  ( F `  Y
) )  +  ( ( 1  -  (
1  -  T ) )  x.  ( F `
 X ) ) )  =  ( ( ( 1  -  T
)  x.  ( F `
 Y ) )  +  ( T  x.  ( F `  X ) ) ) )
171160, 80remulcld 9010 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  -  T )  x.  ( F `  Y )
)  e.  RR )
172171recnd 9008 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  -  T )  x.  ( F `  Y )
)  e.  CC )
173 ffvelrn 5770 . . . . . . . . . . . . . . 15  |-  ( ( F : D --> RR  /\  X  e.  D )  ->  ( F `  X
)  e.  RR )
17478, 3, 173syl2anc 642 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  X
)  e.  RR )
17563, 174remulcld 9010 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( T  x.  ( F `  X )
)  e.  RR )
176175recnd 9008 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( T  x.  ( F `  X )
)  e.  CC )
177172, 176addcomd 9161 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( ( 1  -  T )  x.  ( F `  Y
) )  +  ( T  x.  ( F `
 X ) ) )  =  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) ) )
178170, 177eqtrd 2398 . . . . . . . . . 10  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( ( 1  -  T )  x.  ( F `  Y
) )  +  ( ( 1  -  (
1  -  T ) )  x.  ( F `
 X ) ) )  =  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) ) )
179178adantr 451 . . . . . . . . 9  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  Y  <  X ) )  -> 
( ( ( 1  -  T )  x.  ( F `  Y
) )  +  ( ( 1  -  (
1  -  T ) )  x.  ( F `
 X ) ) )  =  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) ) )
180155, 168, 1793brtr3d 4154 . . . . . . . 8  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  Y  <  X ) )  -> 
( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  <  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) ) )
181180orcd 381 . . . . . . 7  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  ( T  e.  ( 0 (,) 1 )  /\  Y  <  X ) )  -> 
( ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  <  (
( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  \/  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  =  ( ( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) ) ) )
182181expr 598 . . . . . 6  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  T  e.  ( 0 (,) 1
) )  ->  ( Y  <  X  ->  (
( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  <  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) )  \/  ( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) ) ) ) )
18357, 96, 1823jaod 1247 . . . . 5  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  T  e.  ( 0 (,) 1
) )  ->  (
( X  <  Y  \/  X  =  Y  \/  Y  <  X )  ->  ( ( F `
 ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y
) ) )  < 
( ( T  x.  ( F `  X ) )  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  \/  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  =  ( ( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) ) ) ) )
1849, 183mpd 14 . . . 4  |-  ( ( ( ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1 ) ) )  /\  T  e.  ( 0 (,) 1
) )  ->  (
( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  <  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) )  \/  ( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) ) ) )
185184ex 423 . . 3  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( T  e.  ( 0 (,) 1 )  ->  ( ( F `
 ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y
) ) )  < 
( ( T  x.  ( F `  X ) )  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  \/  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  =  ( ( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) ) ) ) )
186 elpri 3749 . . . 4  |-  ( T  e.  { 0 ,  1 }  ->  ( T  =  0  \/  T  =  1 ) )
18781addid2d 9160 . . . . . . 7  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 0  +  ( F `  Y ) )  =  ( F `
 Y ) )
188174recnd 9008 . . . . . . . . 9  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  X
)  e.  CC )
189188mul02d 9157 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 0  x.  ( F `  X )
)  =  0 )
190189, 83oveq12d 5999 . . . . . . 7  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 0  x.  ( F `  X
) )  +  ( 1  x.  ( F `
 Y ) ) )  =  ( 0  +  ( F `  Y ) ) )
1914recnd 9008 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  X  e.  CC )
192191mul02d 9157 . . . . . . . . . 10  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 0  x.  X
)  =  0 )
193192, 73oveq12d 5999 . . . . . . . . 9  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 0  x.  X )  +  ( 1  x.  Y ) )  =  ( 0  +  Y ) )
19471addid2d 9160 . . . . . . . . 9  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 0  +  Y
)  =  Y )
195193, 194eqtrd 2398 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 0  x.  X )  +  ( 1  x.  Y ) )  =  Y )
196195fveq2d 5636 . . . . . . 7  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  (
( 0  x.  X
)  +  ( 1  x.  Y ) ) )  =  ( F `
 Y ) )
197187, 190, 1963eqtr4rd 2409 . . . . . 6  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  (
( 0  x.  X
)  +  ( 1  x.  Y ) ) )  =  ( ( 0  x.  ( F `
 X ) )  +  ( 1  x.  ( F `  Y
) ) ) )
198 oveq1 5988 . . . . . . . . 9  |-  ( T  =  0  ->  ( T  x.  X )  =  ( 0  x.  X ) )
199 oveq2 5989 . . . . . . . . . . 11  |-  ( T  =  0  ->  (
1  -  T )  =  ( 1  -  0 ) )
20065subid1i 9265 . . . . . . . . . . 11  |-  ( 1  -  0 )  =  1
201199, 200syl6eq 2414 . . . . . . . . . 10  |-  ( T  =  0  ->  (
1  -  T )  =  1 )
202201oveq1d 5996 . . . . . . . . 9  |-  ( T  =  0  ->  (
( 1  -  T
)  x.  Y )  =  ( 1  x.  Y ) )
203198, 202oveq12d 5999 . . . . . . . 8  |-  ( T  =  0  ->  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) )  =  ( ( 0  x.  X )  +  ( 1  x.  Y
) ) )
204203fveq2d 5636 . . . . . . 7  |-  ( T  =  0  ->  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( F `  ( ( 0  x.  X )  +  ( 1  x.  Y ) ) ) )
205 oveq1 5988 . . . . . . . 8  |-  ( T  =  0  ->  ( T  x.  ( F `  X ) )  =  ( 0  x.  ( F `  X )
) )
206201oveq1d 5996 . . . . . . . 8  |-  ( T  =  0  ->  (
( 1  -  T
)  x.  ( F `
 Y ) )  =  ( 1  x.  ( F `  Y
) ) )
207205, 206oveq12d 5999 . . . . . . 7  |-  ( T  =  0  ->  (
( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  =  ( ( 0  x.  ( F `  X ) )  +  ( 1  x.  ( F `  Y )
) ) )
208204, 207eqeq12d 2380 . . . . . 6  |-  ( T  =  0  ->  (
( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) )  <->  ( F `  ( ( 0  x.  X )  +  ( 1  x.  Y ) ) )  =  ( ( 0  x.  ( F `  X )
)  +  ( 1  x.  ( F `  Y ) ) ) ) )
209197, 208syl5ibrcom 213 . . . . 5  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( T  =  0  ->  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  =  ( ( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) ) ) )
210188addid1d 9159 . . . . . . 7  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( F `  X )  +  0 )  =  ( F `
 X ) )
211188mulid2d 9000 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 1  x.  ( F `  X )
)  =  ( F `
 X ) )
21281mul02d 9157 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 0  x.  ( F `  Y )
)  =  0 )
213211, 212oveq12d 5999 . . . . . . 7  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  x.  ( F `  X
) )  +  ( 0  x.  ( F `
 Y ) ) )  =  ( ( F `  X )  +  0 ) )
214191mulid2d 9000 . . . . . . . . . 10  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 1  x.  X
)  =  X )
21571mul02d 9157 . . . . . . . . . 10  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 0  x.  Y
)  =  0 )
216214, 215oveq12d 5999 . . . . . . . . 9  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  x.  X )  +  ( 0  x.  Y ) )  =  ( X  +  0 ) )
217191addid1d 9159 . . . . . . . . 9  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( X  +  0 )  =  X )
218216, 217eqtrd 2398 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  x.  X )  +  ( 0  x.  Y ) )  =  X )
219218fveq2d 5636 . . . . . . 7  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  (
( 1  x.  X
)  +  ( 0  x.  Y ) ) )  =  ( F `
 X ) )
220210, 213, 2193eqtr4rd 2409 . . . . . 6  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  (
( 1  x.  X
)  +  ( 0  x.  Y ) ) )  =  ( ( 1  x.  ( F `
 X ) )  +  ( 0  x.  ( F `  Y
) ) ) )
221 oveq1 5988 . . . . . . . . 9  |-  ( T  =  1  ->  ( T  x.  X )  =  ( 1  x.  X ) )
222 oveq2 5989 . . . . . . . . . . 11  |-  ( T  =  1  ->  (
1  -  T )  =  ( 1  -  1 ) )
223 1m1e0 9961 . . . . . . . . . . 11  |-  ( 1  -  1 )  =  0
224222, 223syl6eq 2414 . . . . . . . . . 10  |-  ( T  =  1  ->  (
1  -  T )  =  0 )
225224oveq1d 5996 . . . . . . . . 9  |-  ( T  =  1  ->  (
( 1  -  T
)  x.  Y )  =  ( 0  x.  Y ) )
226221, 225oveq12d 5999 . . . . . . . 8  |-  ( T  =  1  ->  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) )  =  ( ( 1  x.  X )  +  ( 0  x.  Y
) ) )
227226fveq2d 5636 . . . . . . 7  |-  ( T  =  1  ->  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( F `  ( ( 1  x.  X )  +  ( 0  x.  Y ) ) ) )
228 oveq1 5988 . . . . . . . 8  |-  ( T  =  1  ->  ( T  x.  ( F `  X ) )  =  ( 1  x.  ( F `  X )
) )
229224oveq1d 5996 . . . . . . . 8  |-  ( T  =  1  ->  (
( 1  -  T
)  x.  ( F `
 Y ) )  =  ( 0  x.  ( F `  Y
) ) )
230228, 229oveq12d 5999 . . . . . . 7  |-  ( T  =  1  ->  (
( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  =  ( ( 1  x.  ( F `  X ) )  +  ( 0  x.  ( F `  Y )
) ) )
231227, 230eqeq12d 2380 . . . . . 6  |-  ( T  =  1  ->  (
( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( ( T  x.  ( F `
 X ) )  +  ( ( 1  -  T )  x.  ( F `  Y
) ) )  <->  ( F `  ( ( 1  x.  X )  +  ( 0  x.  Y ) ) )  =  ( ( 1  x.  ( F `  X )
)  +  ( 0  x.  ( F `  Y ) ) ) ) )
232220, 231syl5ibrcom 213 . . . . 5  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( T  =  1  ->  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  =  ( ( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) ) ) )
233209, 232jaod 369 . . . 4  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( T  =  0  \/  T  =  1 )  ->  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( ( T  x.  ( F `  X ) )  +  ( ( 1  -  T )  x.  ( F `  Y )
) ) ) )
234186, 233, 95syl56 30 . . 3  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( T  e.  {
0 ,  1 }  ->  ( ( F `
 ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y
) ) )  < 
( ( T  x.  ( F `  X ) )  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  \/  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  =  ( ( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) ) ) ) )
235 0le1 9444 . . . . . 6  |-  0  <_  1
236 prunioo 10917 . . . . . 6  |-  ( ( 0  e.  RR*  /\  1  e.  RR*  /\  0  <_ 
1 )  ->  (
( 0 (,) 1
)  u.  { 0 ,  1 } )  =  ( 0 [,] 1 ) )
237109, 111, 235, 236mp3an 1278 . . . . 5  |-  ( ( 0 (,) 1 )  u.  { 0 ,  1 } )  =  ( 0 [,] 1
)
23862, 237syl6eleqr 2457 . . . 4  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  T  e.  ( (
0 (,) 1 )  u.  { 0 ,  1 } ) )
239 elun 3404 . . . 4  |-  ( T  e.  ( ( 0 (,) 1 )  u. 
{ 0 ,  1 } )  <->  ( T  e.  ( 0 (,) 1
)  \/  T  e. 
{ 0 ,  1 } ) )
240238, 239sylib 188 . . 3  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( T  e.  ( 0 (,) 1 )  \/  T  e.  {
0 ,  1 } ) )
241185, 234, 240mpjaod 370 . 2  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  <  (
( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  \/  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  =  ( ( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) ) ) )
242 scvxcvx.3 . . . . 5  |-  ( (
ph  /\  ( a  e.  D  /\  b  e.  D ) )  -> 
( a [,] b
)  C_  D )
2431, 242cvxcl 20501 . . . 4  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) )  e.  D )
244 ffvelrn 5770 . . . 4  |-  ( ( F : D --> RR  /\  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) )  e.  D )  ->  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  e.  RR )
24578, 243, 244syl2anc 642 . . 3  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  e.  RR )
246175, 171readdcld 9009 . . 3  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( T  x.  ( F `  X ) )  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  e.  RR )
247245, 246leloed 9109 . 2  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  <_  (
( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  <-> 
( ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  <  (
( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  \/  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) )  =  ( ( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) ) ) ) )
248241, 247mpbird 223 1  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) ) )  <_  ( ( T  x.  ( F `  X ) )  +  ( ( 1  -  T )  x.  ( F `  Y )
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    \/ w3o 934    /\ w3a 935    = wceq 1647    e. wcel 1715   A.wral 2628    u. cun 3236    C_ wss 3238   {cpr 3730   class class class wbr 4125   -->wf 5354   ` cfv 5358  (class class class)co 5981   CCcc 8882   RRcr 8883   0cc0 8884   1c1 8885    + caddc 8887    x. cmul 8889   RR*cxr 9013    < clt 9014    <_ cle 9015    - cmin 9184   (,)cioo 10809   [,]cicc 10812
This theorem is referenced by:  amgmlem  20506
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316  ax-un 4615  ax-cnex 8940  ax-resscn 8941  ax-1cn 8942  ax-icn 8943  ax-addcl 8944  ax-addrcl 8945  ax-mulcl 8946  ax-mulrcl 8947  ax-mulcom 8948  ax-addass 8949  ax-mulass 8950  ax-distr 8951  ax-i2m1 8952  ax-1ne0 8953  ax-1rid 8954  ax-rnegex 8955  ax-rrecex 8956  ax-cnre 8957  ax-pre-lttri 8958  ax-pre-lttrn 8959  ax-pre-ltadd 8960  ax-pre-mulgt0 8961  ax-pre-sup 8962
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 936  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-nel 2532  df-ral 2633  df-rex 2634  df-reu 2635  df-rmo 2636  df-rab 2637  df-v 2875  df-sbc 3078  df-csb 3168  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-pss 3254  df-nul 3544  df-if 3655  df-pw 3716  df-sn 3735  df-pr 3736  df-tp 3737  df-op 3738  df-uni 3930  df-iun 4009  df-br 4126  df-opab 4180  df-mpt 4181  df-tr 4216  df-eprel 4408  df-id 4412  df-po 4417  df-so 4418  df-fr 4455  df-we 4457  df-ord 4498  df-on 4499  df-lim 4500  df-suc 4501  df-om 4760  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-f1 5363  df-fo 5364  df-f1o 5365  df-fv 5366  df-ov 5984  df-oprab 5985  df-mpt2 5986  df-1st 6249  df-2nd 6250  df-riota 6446  df-recs 6530  df-rdg 6565  df-er 6802  df-en 7007  df-dom 7008  df-sdom 7009  df-sup 7341  df-pnf 9016  df-mnf 9017  df-xr 9018  df-ltxr 9019  df-le 9020  df-sub 9186  df-neg 9187  df-div 9571  df-nn 9894  df-n0 10115  df-z 10176  df-uz 10382  df-q 10468  df-rp 10506  df-ioo 10813  df-ico 10815  df-icc 10816
  Copyright terms: Public domain W3C validator