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

Theorem scvxcvx 20280
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 961 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  X  e.  D )
42, 3sseldd 3181 . . . . . . 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 962 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  Y  e.  D )
72, 6sseldd 3181 . . . . . . 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 8960 . . . . 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 4026 . . . . . . . . . . . 12  |-  ( x  =  X  ->  (
x  <  y  <->  X  <  y ) )
17 oveq2 5866 . . . . . . . . . . . . . . . . 17  |-  ( x  =  X  ->  (
t  x.  x )  =  ( t  x.  X ) )
1817oveq1d 5873 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  (
( t  x.  x
)  +  ( ( 1  -  t )  x.  y ) )  =  ( ( t  x.  X )  +  ( ( 1  -  t )  x.  y
) ) )
1918fveq2d 5529 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  ( F `  ( (
t  x.  x )  +  ( ( 1  -  t )  x.  y ) ) )  =  ( F `  ( ( t  x.  X )  +  ( ( 1  -  t
)  x.  y ) ) ) )
20 fveq2 5525 . . . . . . . . . . . . . . . . 17  |-  ( x  =  X  ->  ( F `  x )  =  ( F `  X ) )
2120oveq2d 5874 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  (
t  x.  ( F `
 x ) )  =  ( t  x.  ( F `  X
) ) )
2221oveq1d 5873 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
( t  x.  ( F `  x )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) )  =  ( ( t  x.  ( F `  X ) )  +  ( ( 1  -  t )  x.  ( F `  y )
) ) )
2319, 22breq12d 4036 . . . . . . . . . . . . . 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 2563 . . . . . . . . . . . . 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 4027 . . . . . . . . . . . 12  |-  ( y  =  Y  ->  ( X  <  y  <->  X  <  Y ) )
28 oveq2 5866 . . . . . . . . . . . . . . . . 17  |-  ( y  =  Y  ->  (
( 1  -  t
)  x.  y )  =  ( ( 1  -  t )  x.  Y ) )
2928oveq2d 5874 . . . . . . . . . . . . . . . 16  |-  ( y  =  Y  ->  (
( t  x.  X
)  +  ( ( 1  -  t )  x.  y ) )  =  ( ( t  x.  X )  +  ( ( 1  -  t )  x.  Y
) ) )
3029fveq2d 5529 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  ( F `  ( (
t  x.  X )  +  ( ( 1  -  t )  x.  y ) ) )  =  ( F `  ( ( t  x.  X )  +  ( ( 1  -  t
)  x.  Y ) ) ) )
31 fveq2 5525 . . . . . . . . . . . . . . . . 17  |-  ( y  =  Y  ->  ( F `  y )  =  ( F `  Y ) )
3231oveq2d 5874 . . . . . . . . . . . . . . . 16  |-  ( y  =  Y  ->  (
( 1  -  t
)  x.  ( F `
 y ) )  =  ( ( 1  -  t )  x.  ( F `  Y
) ) )
3332oveq2d 5874 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  (
( t  x.  ( F `  X )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) )  =  ( ( t  x.  ( F `  X ) )  +  ( ( 1  -  t )  x.  ( F `  Y )
) ) )
3430, 33breq12d 4036 . . . . . . . . . . . . . 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 2563 . . . . . . . . . . . . 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 1153 . . . . . . . . . . . . . 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 2625 . . . . . . . . . . . . 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 1153 . . . . . . . . . . 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 2851 . . . . . . . . . 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 5865 . . . . . . . . . . . . 13  |-  ( t  =  T  ->  (
t  x.  X )  =  ( T  x.  X ) )
46 oveq2 5866 . . . . . . . . . . . . . 14  |-  ( t  =  T  ->  (
1  -  t )  =  ( 1  -  T ) )
4746oveq1d 5873 . . . . . . . . . . . . 13  |-  ( t  =  T  ->  (
( 1  -  t
)  x.  Y )  =  ( ( 1  -  T )  x.  Y ) )
4845, 47oveq12d 5876 . . . . . . . . . . . 12  |-  ( t  =  T  ->  (
( t  x.  X
)  +  ( ( 1  -  t )  x.  Y ) )  =  ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y
) ) )
4948fveq2d 5529 . . . . . . . . . . 11  |-  ( t  =  T  ->  ( F `  ( (
t  x.  X )  +  ( ( 1  -  t )  x.  Y ) ) )  =  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) ) ) )
50 oveq1 5865 . . . . . . . . . . . 12  |-  ( t  =  T  ->  (
t  x.  ( F `
 X ) )  =  ( T  x.  ( F `  X ) ) )
5146oveq1d 5873 . . . . . . . . . . . 12  |-  ( t  =  T  ->  (
( 1  -  t
)  x.  ( F `
 Y ) )  =  ( ( 1  -  T )  x.  ( F `  Y
) ) )
5250, 51oveq12d 5876 . . . . . . . . . . 11  |-  ( t  =  T  ->  (
( t  x.  ( F `  X )
)  +  ( ( 1  -  t )  x.  ( F `  Y ) ) )  =  ( ( T  x.  ( F `  X ) )  +  ( ( 1  -  T )  x.  ( F `  Y )
) ) )
5349, 52breq12d 4036 . . . . . . . . . 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 2880 . . . . . . . . 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 8838 . . . . . . . . . . . . . . . . 17  |-  0  e.  RR
59 1re 8837 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR
60 iccssre 10731 . . . . . . . . . . . . . . . . 17  |-  ( ( 0  e.  RR  /\  1  e.  RR )  ->  ( 0 [,] 1
)  C_  RR )
6158, 59, 60mp2an 653 . . . . . . . . . . . . . . . 16  |-  ( 0 [,] 1 )  C_  RR
62 simpr3 963 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  T  e.  ( 0 [,] 1 ) )
6361, 62sseldi 3178 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  T  e.  RR )
6463recnd 8861 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  T  e.  CC )
65 ax-1cn 8795 . . . . . . . . . . . . . 14  |-  1  e.  CC
66 pncan3 9059 . . . . . . . . . . . . . 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 5873 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( T  +  ( 1  -  T
) )  x.  Y
)  =  ( 1  x.  Y ) )
69 subcl 9051 . . . . . . . . . . . . . 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 8861 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  Y  e.  CC )
7264, 70, 71adddird 8860 . . . . . . . . . . . 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 8853 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 1  x.  Y
)  =  Y )
7468, 72, 733eqtr3d 2323 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( T  x.  Y )  +  ( ( 1  -  T
)  x.  Y ) )  =  Y )
7574fveq2d 5529 . . . . . . . . . 10  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  (
( T  x.  Y
)  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( F `
 Y ) )
7667oveq1d 5873 . . . . . . . . . . 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 5663 . . . . . . . . . . . . . 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 8861 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  Y
)  e.  CC )
8264, 70, 81adddird 8860 . . . . . . . . . . 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 8853 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 1  x.  ( F `  Y )
)  =  ( F `
 Y ) )
8476, 82, 833eqtr3d 2323 . . . . . . . . . 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 2318 . . . . . . . . 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 5866 . . . . . . . . . . 11  |-  ( X  =  Y  ->  ( T  x.  X )  =  ( T  x.  Y ) )
8887oveq1d 5873 . . . . . . . . . 10  |-  ( X  =  Y  ->  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) )  =  ( ( T  x.  Y )  +  ( ( 1  -  T )  x.  Y
) ) )
8988fveq2d 5529 . . . . . . . . 9  |-  ( X  =  Y  ->  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( F `  ( ( T  x.  Y )  +  ( ( 1  -  T
)  x.  Y ) ) ) )
90 fveq2 5525 . . . . . . . . . . 11  |-  ( X  =  Y  ->  ( F `  X )  =  ( F `  Y ) )
9190oveq2d 5874 . . . . . . . . . 10  |-  ( X  =  Y  ->  ( T  x.  ( F `  X ) )  =  ( T  x.  ( F `  Y )
) )
9291oveq1d 5873 . . . . . . . . 9  |-  ( X  =  Y  ->  (
( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  =  ( ( T  x.  ( F `  Y ) )  +  ( ( 1  -  T )  x.  ( F `  Y )
) ) )
9389, 92eqeq12d 2297 . . . . . . . 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 10686 . . . . . . . . . . . . 13  |-  ( T  e.  ( 0 (,) 1 )  ->  T  e.  RR )
98 resubcl 9111 . . . . . . . . . . . . 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 10710 . . . . . . . . . . . . . 14  |-  ( T  e.  ( 0 (,) 1 )  ->  (
0  <  T  /\  T  <  1 ) )
101100simprd 449 . . . . . . . . . . . . 13  |-  ( T  e.  ( 0 (,) 1 )  ->  T  <  1 )
102 posdif 9267 . . . . . . . . . . . . . 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 9266 . . . . . . . . . . . . . 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 8878 . . . . . . . . . . . . 13  |-  0  e.  RR*
110 ressxr 8876 . . . . . . . . . . . . . 14  |-  RR  C_  RR*
111110, 59sselii 3177 . . . . . . . . . . . . 13  |-  1  e.  RR*
112 elioo2 10697 . . . . . . . . . . . . 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 1136 . . . . . . . . . . 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 4026 . . . . . . . . . . . . 13  |-  ( x  =  Y  ->  (
x  <  y  <->  Y  <  y ) )
122 oveq2 5866 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  Y  ->  (
t  x.  x )  =  ( t  x.  Y ) )
123122oveq1d 5873 . . . . . . . . . . . . . . . . 17  |-  ( x  =  Y  ->  (
( t  x.  x
)  +  ( ( 1  -  t )  x.  y ) )  =  ( ( t  x.  Y )  +  ( ( 1  -  t )  x.  y
) ) )
124123fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( x  =  Y  ->  ( F `  ( (
t  x.  x )  +  ( ( 1  -  t )  x.  y ) ) )  =  ( F `  ( ( t  x.  Y )  +  ( ( 1  -  t
)  x.  y ) ) ) )
125 fveq2 5525 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  Y  ->  ( F `  x )  =  ( F `  Y ) )
126125oveq2d 5874 . . . . . . . . . . . . . . . . 17  |-  ( x  =  Y  ->  (
t  x.  ( F `
 x ) )  =  ( t  x.  ( F `  Y
) ) )
127126oveq1d 5873 . . . . . . . . . . . . . . . 16  |-  ( x  =  Y  ->  (
( t  x.  ( F `  x )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) )  =  ( ( t  x.  ( F `  Y ) )  +  ( ( 1  -  t )  x.  ( F `  y )
) ) )
128124, 127breq12d 4036 . . . . . . . . . . . . . . 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 2563 . . . . . . . . . . . . . 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 4027 . . . . . . . . . . . . 13  |-  ( y  =  X  ->  ( Y  <  y  <->  Y  <  X ) )
133 oveq2 5866 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  X  ->  (
( 1  -  t
)  x.  y )  =  ( ( 1  -  t )  x.  X ) )
134133oveq2d 5874 . . . . . . . . . . . . . . . . 17  |-  ( y  =  X  ->  (
( t  x.  Y
)  +  ( ( 1  -  t )  x.  y ) )  =  ( ( t  x.  Y )  +  ( ( 1  -  t )  x.  X
) ) )
135134fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( y  =  X  ->  ( F `  ( (
t  x.  Y )  +  ( ( 1  -  t )  x.  y ) ) )  =  ( F `  ( ( t  x.  Y )  +  ( ( 1  -  t
)  x.  X ) ) ) )
136 fveq2 5525 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  X  ->  ( F `  y )  =  ( F `  X ) )
137136oveq2d 5874 . . . . . . . . . . . . . . . . 17  |-  ( y  =  X  ->  (
( 1  -  t
)  x.  ( F `
 y ) )  =  ( ( 1  -  t )  x.  ( F `  X
) ) )
138137oveq2d 5874 . . . . . . . . . . . . . . . 16  |-  ( y  =  X  ->  (
( t  x.  ( F `  Y )
)  +  ( ( 1  -  t )  x.  ( F `  y ) ) )  =  ( ( t  x.  ( F `  Y ) )  +  ( ( 1  -  t )  x.  ( F `  X )
) ) )
139135, 138breq12d 4036 . . . . . . . . . . . . . . 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 2563 . . . . . . . . . . . . . 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 2851 . . . . . . . . . . 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 5865 . . . . . . . . . . . . . 14  |-  ( t  =  ( 1  -  T )  ->  (
t  x.  Y )  =  ( ( 1  -  T )  x.  Y ) )
146 oveq2 5866 . . . . . . . . . . . . . . 15  |-  ( t  =  ( 1  -  T )  ->  (
1  -  t )  =  ( 1  -  ( 1  -  T
) ) )
147146oveq1d 5873 . . . . . . . . . . . . . 14  |-  ( t  =  ( 1  -  T )  ->  (
( 1  -  t
)  x.  X )  =  ( ( 1  -  ( 1  -  T ) )  x.  X ) )
148145, 147oveq12d 5876 . . . . . . . . . . . . 13  |-  ( t  =  ( 1  -  T )  ->  (
( t  x.  Y
)  +  ( ( 1  -  t )  x.  X ) )  =  ( ( ( 1  -  T )  x.  Y )  +  ( ( 1  -  ( 1  -  T
) )  x.  X
) ) )
149148fveq2d 5529 . . . . . . . . . . . 12  |-  ( t  =  ( 1  -  T )  ->  ( F `  ( (
t  x.  Y )  +  ( ( 1  -  t )  x.  X ) ) )  =  ( F `  ( ( ( 1  -  T )  x.  Y )  +  ( ( 1  -  (
1  -  T ) )  x.  X ) ) ) )
150 oveq1 5865 . . . . . . . . . . . . 13  |-  ( t  =  ( 1  -  T )  ->  (
t  x.  ( F `
 Y ) )  =  ( ( 1  -  T )  x.  ( F `  Y
) ) )
151146oveq1d 5873 . . . . . . . . . . . . 13  |-  ( t  =  ( 1  -  T )  ->  (
( 1  -  t
)  x.  ( F `
 X ) )  =  ( ( 1  -  ( 1  -  T ) )  x.  ( F `  X
) ) )
152150, 151oveq12d 5876 . . . . . . . . . . . 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 4036 . . . . . . . . . . 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 2880 . . . . . . . . . 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 9076 . . . . . . . . . . . . . . 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 5873 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  -  ( 1  -  T
) )  x.  X
)  =  ( T  x.  X ) )
159158oveq2d 5874 . . . . . . . . . . . 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 8863 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  -  T )  x.  Y
)  e.  RR )
162161recnd 8861 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  -  T )  x.  Y
)  e.  CC )
16363, 4remulcld 8863 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( T  x.  X
)  e.  RR )
164163recnd 8861 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( T  x.  X
)  e.  CC )
165162, 164addcomd 9014 . . . . . . . . . . . 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 2315 . . . . . . . . . . 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 5529 . . . . . . . . 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 5873 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  -  ( 1  -  T
) )  x.  ( F `  X )
)  =  ( T  x.  ( F `  X ) ) )
170169oveq2d 5874 . . . . . . . . . . 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 8863 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  -  T )  x.  ( F `  Y )
)  e.  RR )
172171recnd 8861 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  -  T )  x.  ( F `  Y )
)  e.  CC )
173 ffvelrn 5663 . . . . . . . . . . . . . . 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 8863 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( T  x.  ( F `  X )
)  e.  RR )
176175recnd 8861 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( T  x.  ( F `  X )
)  e.  CC )
177172, 176addcomd 9014 . . . . . . . . . . 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 2315 . . . . . . . . . 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 4052 . . . . . . . 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 1246 . . . . 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 3660 . . . 4  |-  ( T  e.  { 0 ,  1 }  ->  ( T  =  0  \/  T  =  1 ) )
18781addid2d 9013 . . . . . . 7  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 0  +  ( F `  Y ) )  =  ( F `
 Y ) )
188174recnd 8861 . . . . . . . . 9  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  X
)  e.  CC )
189188mul02d 9010 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 0  x.  ( F `  X )
)  =  0 )
190189, 83oveq12d 5876 . . . . . . 7  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 0  x.  ( F `  X
) )  +  ( 1  x.  ( F `
 Y ) ) )  =  ( 0  +  ( F `  Y ) ) )
1914recnd 8861 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  X  e.  CC )
192191mul02d 9010 . . . . . . . . . 10  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 0  x.  X
)  =  0 )
193192, 73oveq12d 5876 . . . . . . . . 9  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 0  x.  X )  +  ( 1  x.  Y ) )  =  ( 0  +  Y ) )
19471addid2d 9013 . . . . . . . . 9  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 0  +  Y
)  =  Y )
195193, 194eqtrd 2315 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 0  x.  X )  +  ( 1  x.  Y ) )  =  Y )
196195fveq2d 5529 . . . . . . 7  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  (
( 0  x.  X
)  +  ( 1  x.  Y ) ) )  =  ( F `
 Y ) )
197187, 190, 1963eqtr4rd 2326 . . . . . 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 5865 . . . . . . . . 9  |-  ( T  =  0  ->  ( T  x.  X )  =  ( 0  x.  X ) )
199 oveq2 5866 . . . . . . . . . . 11  |-  ( T  =  0  ->  (
1  -  T )  =  ( 1  -  0 ) )
20065subid1i 9118 . . . . . . . . . . 11  |-  ( 1  -  0 )  =  1
201199, 200syl6eq 2331 . . . . . . . . . 10  |-  ( T  =  0  ->  (
1  -  T )  =  1 )
202201oveq1d 5873 . . . . . . . . 9  |-  ( T  =  0  ->  (
( 1  -  T
)  x.  Y )  =  ( 1  x.  Y ) )
203198, 202oveq12d 5876 . . . . . . . 8  |-  ( T  =  0  ->  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) )  =  ( ( 0  x.  X )  +  ( 1  x.  Y
) ) )
204203fveq2d 5529 . . . . . . 7  |-  ( T  =  0  ->  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( F `  ( ( 0  x.  X )  +  ( 1  x.  Y ) ) ) )
205 oveq1 5865 . . . . . . . 8  |-  ( T  =  0  ->  ( T  x.  ( F `  X ) )  =  ( 0  x.  ( F `  X )
) )
206201oveq1d 5873 . . . . . . . 8  |-  ( T  =  0  ->  (
( 1  -  T
)  x.  ( F `
 Y ) )  =  ( 1  x.  ( F `  Y
) ) )
207205, 206oveq12d 5876 . . . . . . 7  |-  ( T  =  0  ->  (
( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  =  ( ( 0  x.  ( F `  X ) )  +  ( 1  x.  ( F `  Y )
) ) )
208204, 207eqeq12d 2297 . . . . . 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 9012 . . . . . . 7  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( F `  X )  +  0 )  =  ( F `
 X ) )
211188mulid2d 8853 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 1  x.  ( F `  X )
)  =  ( F `
 X ) )
21281mul02d 9010 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 0  x.  ( F `  Y )
)  =  0 )
213211, 212oveq12d 5876 . . . . . . 7  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  x.  ( F `  X
) )  +  ( 0  x.  ( F `
 Y ) ) )  =  ( ( F `  X )  +  0 ) )
214191mulid2d 8853 . . . . . . . . . 10  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 1  x.  X
)  =  X )
21571mul02d 9010 . . . . . . . . . 10  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( 0  x.  Y
)  =  0 )
216214, 215oveq12d 5876 . . . . . . . . 9  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  x.  X )  +  ( 0  x.  Y ) )  =  ( X  +  0 ) )
217191addid1d 9012 . . . . . . . . 9  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( X  +  0 )  =  X )
218216, 217eqtrd 2315 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( 1  x.  X )  +  ( 0  x.  Y ) )  =  X )
219218fveq2d 5529 . . . . . . 7  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( F `  (
( 1  x.  X
)  +  ( 0  x.  Y ) ) )  =  ( F `
 X ) )
220210, 213, 2193eqtr4rd 2326 . . . . . 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 5865 . . . . . . . . 9  |-  ( T  =  1  ->  ( T  x.  X )  =  ( 1  x.  X ) )
222 oveq2 5866 . . . . . . . . . . 11  |-  ( T  =  1  ->  (
1  -  T )  =  ( 1  -  1 ) )
223 1m1e0 9814 . . . . . . . . . . 11  |-  ( 1  -  1 )  =  0
224222, 223syl6eq 2331 . . . . . . . . . 10  |-  ( T  =  1  ->  (
1  -  T )  =  0 )
225224oveq1d 5873 . . . . . . . . 9  |-  ( T  =  1  ->  (
( 1  -  T
)  x.  Y )  =  ( 0  x.  Y ) )
226221, 225oveq12d 5876 . . . . . . . 8  |-  ( T  =  1  ->  (
( T  x.  X
)  +  ( ( 1  -  T )  x.  Y ) )  =  ( ( 1  x.  X )  +  ( 0  x.  Y
) ) )
227226fveq2d 5529 . . . . . . 7  |-  ( T  =  1  ->  ( F `  ( ( T  x.  X )  +  ( ( 1  -  T )  x.  Y ) ) )  =  ( F `  ( ( 1  x.  X )  +  ( 0  x.  Y ) ) ) )
228 oveq1 5865 . . . . . . . 8  |-  ( T  =  1  ->  ( T  x.  ( F `  X ) )  =  ( 1  x.  ( F `  X )
) )
229224oveq1d 5873 . . . . . . . 8  |-  ( T  =  1  ->  (
( 1  -  T
)  x.  ( F `
 Y ) )  =  ( 0  x.  ( F `  Y
) ) )
230228, 229oveq12d 5876 . . . . . . 7  |-  ( T  =  1  ->  (
( T  x.  ( F `  X )
)  +  ( ( 1  -  T )  x.  ( F `  Y ) ) )  =  ( ( 1  x.  ( F `  X ) )  +  ( 0  x.  ( F `  Y )
) ) )
231227, 230eqeq12d 2297 . . . . . 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 9297 . . . . . 6  |-  0  <_  1
236 prunioo 10764 . . . . . 6  |-  ( ( 0  e.  RR*  /\  1  e.  RR*  /\  0  <_ 
1 )  ->  (
( 0 (,) 1
)  u.  { 0 ,  1 } )  =  ( 0 [,] 1 ) )
237109, 111, 235, 236mp3an 1277 . . . . 5  |-  ( ( 0 (,) 1 )  u.  { 0 ,  1 } )  =  ( 0 [,] 1
)
23862, 237syl6eleqr 2374 . . . 4  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  ->  T  e.  ( (
0 (,) 1 )  u.  { 0 ,  1 } ) )
239 elun 3316 . . . 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 20279 . . . 4  |-  ( (
ph  /\  ( X  e.  D  /\  Y  e.  D  /\  T  e.  ( 0 [,] 1
) ) )  -> 
( ( T  x.  X )  +  ( ( 1  -  T
)  x.  Y ) )  e.  D )
244 ffvelrn 5663 . . . 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 8862 . . 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 8962 . 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 933    /\ w3a 934    = wceq 1623    e. wcel 1684   A.wral 2543    u. cun 3150    C_ wss 3152   {cpr 3641   class class class wbr 4023   -->wf 5251   ` cfv 5255  (class class class)co 5858   CCcc 8735   RRcr 8736   0cc0 8737   1c1 8738    + caddc 8740    x. cmul 8742   RR*cxr 8866    < clt 8867    <_ cle 8868    - cmin 9037   (,)cioo 10656   [,]cicc 10659
This theorem is referenced by:  amgmlem  20284
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814  ax-pre-sup 8815
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-er 6660  df-en 6864  df-dom 6865  df-sdom 6866  df-sup 7194  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-div 9424  df-nn 9747  df-n0 9966  df-z 10025  df-uz 10231  df-q 10317  df-rp 10355  df-ioo 10660  df-ico 10662  df-icc 10663
  Copyright terms: Public domain W3C validator