Metamath Proof Explorer

Theorem scvxcvx

Description: A strictly convex function is convex. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypotheses 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 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 scvxcvx.1 
 |-  ( ph -> D C_ RR )
2 scvxcvx.2 
 |-  ( ph -> F : D --> RR )
3 scvxcvx.3 
 |-  ( ( ph /\ ( a e. D /\ b e. D ) ) -> ( a [,] b ) C_ D )
4 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 ) ) ) )
5 1 adantr 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> D C_ RR )
6 simpr1 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> X e. D )
7 5 6 sseldd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> X e. RR )
8 7 adantr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ T e. ( 0 (,) 1 ) ) -> X e. RR )
9 simpr2 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> Y e. D )
10 5 9 sseldd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> Y e. RR )
11 10 adantr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ T e. ( 0 (,) 1 ) ) -> Y e. RR )
12 8 11 lttri4d 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ T e. ( 0 (,) 1 ) ) -> ( X < Y \/ X = Y \/ Y < X ) )
13 oveq1 
 |-  ( t = T -> ( t x. X ) = ( T x. X ) )
14 oveq2 
 |-  ( t = T -> ( 1 - t ) = ( 1 - T ) )
15 14 oveq1d 
 |-  ( t = T -> ( ( 1 - t ) x. Y ) = ( ( 1 - T ) x. Y ) )
16 13 15 oveq12d 
 |-  ( t = T -> ( ( t x. X ) + ( ( 1 - t ) x. Y ) ) = ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) )
17 16 fveq2d 
 |-  ( t = T -> ( F ` ( ( t x. X ) + ( ( 1 - t ) x. Y ) ) ) = ( F ` ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) ) )
18 oveq1 
 |-  ( t = T -> ( t x. ( F ` X ) ) = ( T x. ( F ` X ) ) )
19 14 oveq1d 
 |-  ( t = T -> ( ( 1 - t ) x. ( F ` Y ) ) = ( ( 1 - T ) x. ( F ` Y ) ) )
20 18 19 oveq12d 
 |-  ( t = T -> ( ( t x. ( F ` X ) ) + ( ( 1 - t ) x. ( F ` Y ) ) ) = ( ( T x. ( F ` X ) ) + ( ( 1 - T ) x. ( F ` Y ) ) ) )
21 17 20 breq12d 
 |-  ( 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 ) ) ) ) )
22 6 adantr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ ( T e. ( 0 (,) 1 ) /\ X < Y ) ) -> X e. D )
23 9 adantr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ ( T e. ( 0 (,) 1 ) /\ X < Y ) ) -> Y e. D )
24 22 23 jca 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ ( T e. ( 0 (,) 1 ) /\ X < Y ) ) -> ( X e. D /\ Y e. D ) )
25 simprr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ ( T e. ( 0 (,) 1 ) /\ X < Y ) ) -> X < Y )
26 simpll 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ ( T e. ( 0 (,) 1 ) /\ X < Y ) ) -> ph )
27 breq1 
 |-  ( x = X -> ( x < y <-> X < y ) )
28 oveq2 
 |-  ( x = X -> ( t x. x ) = ( t x. X ) )
29 28 fvoveq1d 
 |-  ( x = X -> ( F ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) = ( F ` ( ( t x. X ) + ( ( 1 - t ) x. y ) ) ) )
30 fveq2 
 |-  ( x = X -> ( F ` x ) = ( F ` X ) )
31 30 oveq2d 
 |-  ( x = X -> ( t x. ( F ` x ) ) = ( t x. ( F ` X ) ) )
32 31 oveq1d 
 |-  ( x = X -> ( ( t x. ( F ` x ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) = ( ( t x. ( F ` X ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) )
33 29 32 breq12d 
 |-  ( 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 ) ) ) ) )
34 33 ralbidv 
 |-  ( 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 ) ) ) ) )
35 34 imbi2d 
 |-  ( 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 ) ) ) ) ) )
36 27 35 imbi12d 
 |-  ( 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 ) ) ) ) ) ) )
37 breq2 
 |-  ( y = Y -> ( X < y <-> X < Y ) )
38 oveq2 
 |-  ( y = Y -> ( ( 1 - t ) x. y ) = ( ( 1 - t ) x. Y ) )
39 38 oveq2d 
 |-  ( y = Y -> ( ( t x. X ) + ( ( 1 - t ) x. y ) ) = ( ( t x. X ) + ( ( 1 - t ) x. Y ) ) )
40 39 fveq2d 
 |-  ( y = Y -> ( F ` ( ( t x. X ) + ( ( 1 - t ) x. y ) ) ) = ( F ` ( ( t x. X ) + ( ( 1 - t ) x. Y ) ) ) )
41 fveq2 
 |-  ( y = Y -> ( F ` y ) = ( F ` Y ) )
42 41 oveq2d 
 |-  ( y = Y -> ( ( 1 - t ) x. ( F ` y ) ) = ( ( 1 - t ) x. ( F ` Y ) ) )
43 42 oveq2d 
 |-  ( y = Y -> ( ( t x. ( F ` X ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) = ( ( t x. ( F ` X ) ) + ( ( 1 - t ) x. ( F ` Y ) ) ) )
44 40 43 breq12d 
 |-  ( 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 ) ) ) ) )
45 44 ralbidv 
 |-  ( 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 ) ) ) ) )
46 45 imbi2d 
 |-  ( 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 ) ) ) ) ) )
47 37 46 imbi12d 
 |-  ( 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 ) ) ) ) ) ) )
48 4 3expia 
 |-  ( ( 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 ) ) ) ) )
49 48 ralrimiv 
 |-  ( ( 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 ) ) ) )
50 49 expcom 
 |-  ( ( 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 ) ) ) ) )
51 50 3expia 
 |-  ( ( 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 ) ) ) ) ) )
52 36 47 51 vtocl2ga 
 |-  ( ( 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 ) ) ) ) ) )
53 24 25 26 52 syl3c 
 |-  ( ( ( 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 ) ) ) )
54 simprl 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ ( T e. ( 0 (,) 1 ) /\ X < Y ) ) -> T e. ( 0 (,) 1 ) )
55 21 53 54 rspcdva 
 |-  ( ( ( 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 ) ) ) )
56 55 orcd 
 |-  ( ( ( 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 ) ) ) ) )
57 56 expr 
 |-  ( ( ( 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 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
59 simpr3 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> T e. ( 0 [,] 1 ) )
60 58 59 sseldi 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> T e. RR )
61 60 recnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> T e. CC )
62 ax-1cn 
 |-  1 e. CC
63 pncan3 
 |-  ( ( T e. CC /\ 1 e. CC ) -> ( T + ( 1 - T ) ) = 1 )
64 61 62 63 sylancl 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( T + ( 1 - T ) ) = 1 )
65 64 oveq1d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T + ( 1 - T ) ) x. Y ) = ( 1 x. Y ) )
66 subcl 
 |-  ( ( 1 e. CC /\ T e. CC ) -> ( 1 - T ) e. CC )
67 62 61 66 sylancr 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. CC )
68 10 recnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> Y e. CC )
69 61 67 68 adddird 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T + ( 1 - T ) ) x. Y ) = ( ( T x. Y ) + ( ( 1 - T ) x. Y ) ) )
70 68 mulid2d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 1 x. Y ) = Y )
71 65 69 70 3eqtr3d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. Y ) + ( ( 1 - T ) x. Y ) ) = Y )
72 71 fveq2d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( F ` ( ( T x. Y ) + ( ( 1 - T ) x. Y ) ) ) = ( F ` Y ) )
73 64 oveq1d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T + ( 1 - T ) ) x. ( F ` Y ) ) = ( 1 x. ( F ` Y ) ) )
74 2 adantr 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> F : D --> RR )
75 74 9 ffvelrnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( F ` Y ) e. RR )
76 75 recnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( F ` Y ) e. CC )
77 61 67 76 adddird 
 |-  ( ( 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 ) ) ) )
78 76 mulid2d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 1 x. ( F ` Y ) ) = ( F ` Y ) )
79 73 77 78 3eqtr3d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. ( F ` Y ) ) + ( ( 1 - T ) x. ( F ` Y ) ) ) = ( F ` Y ) )
80 72 79 eqtr4d 
 |-  ( ( 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 ) ) ) )
81 80 adantr 
 |-  ( ( ( 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 ) ) ) )
82 oveq2 
 |-  ( X = Y -> ( T x. X ) = ( T x. Y ) )
83 82 fvoveq1d 
 |-  ( X = Y -> ( F ` ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) ) = ( F ` ( ( T x. Y ) + ( ( 1 - T ) x. Y ) ) ) )
84 fveq2 
 |-  ( X = Y -> ( F ` X ) = ( F ` Y ) )
85 84 oveq2d 
 |-  ( X = Y -> ( T x. ( F ` X ) ) = ( T x. ( F ` Y ) ) )
86 85 oveq1d 
 |-  ( X = Y -> ( ( T x. ( F ` X ) ) + ( ( 1 - T ) x. ( F ` Y ) ) ) = ( ( T x. ( F ` Y ) ) + ( ( 1 - T ) x. ( F ` Y ) ) ) )
87 83 86 eqeq12d 
 |-  ( 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 ) ) ) ) )
88 81 87 syl5ibrcom 
 |-  ( ( ( 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 ) ) ) ) )
89 olc 
 |-  ( ( 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 ) ) ) ) )
90 88 89 syl6 
 |-  ( ( ( 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 ) ) ) ) ) )
91 oveq1 
 |-  ( t = ( 1 - T ) -> ( t x. Y ) = ( ( 1 - T ) x. Y ) )
92 oveq2 
 |-  ( t = ( 1 - T ) -> ( 1 - t ) = ( 1 - ( 1 - T ) ) )
93 92 oveq1d 
 |-  ( t = ( 1 - T ) -> ( ( 1 - t ) x. X ) = ( ( 1 - ( 1 - T ) ) x. X ) )
94 91 93 oveq12d 
 |-  ( t = ( 1 - T ) -> ( ( t x. Y ) + ( ( 1 - t ) x. X ) ) = ( ( ( 1 - T ) x. Y ) + ( ( 1 - ( 1 - T ) ) x. X ) ) )
95 94 fveq2d 
 |-  ( t = ( 1 - T ) -> ( F ` ( ( t x. Y ) + ( ( 1 - t ) x. X ) ) ) = ( F ` ( ( ( 1 - T ) x. Y ) + ( ( 1 - ( 1 - T ) ) x. X ) ) ) )
96 oveq1 
 |-  ( t = ( 1 - T ) -> ( t x. ( F ` Y ) ) = ( ( 1 - T ) x. ( F ` Y ) ) )
97 92 oveq1d 
 |-  ( t = ( 1 - T ) -> ( ( 1 - t ) x. ( F ` X ) ) = ( ( 1 - ( 1 - T ) ) x. ( F ` X ) ) )
98 96 97 oveq12d 
 |-  ( t = ( 1 - T ) -> ( ( t x. ( F ` Y ) ) + ( ( 1 - t ) x. ( F ` X ) ) ) = ( ( ( 1 - T ) x. ( F ` Y ) ) + ( ( 1 - ( 1 - T ) ) x. ( F ` X ) ) ) )
99 95 98 breq12d 
 |-  ( 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 ) ) ) ) )
100 9 adantr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ ( T e. ( 0 (,) 1 ) /\ Y < X ) ) -> Y e. D )
101 6 adantr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ ( T e. ( 0 (,) 1 ) /\ Y < X ) ) -> X e. D )
102 100 101 jca 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ ( T e. ( 0 (,) 1 ) /\ Y < X ) ) -> ( Y e. D /\ X e. D ) )
103 simprr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ ( T e. ( 0 (,) 1 ) /\ Y < X ) ) -> Y < X )
104 simpll 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ ( T e. ( 0 (,) 1 ) /\ Y < X ) ) -> ph )
105 breq1 
 |-  ( x = Y -> ( x < y <-> Y < y ) )
106 oveq2 
 |-  ( x = Y -> ( t x. x ) = ( t x. Y ) )
107 106 fvoveq1d 
 |-  ( x = Y -> ( F ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) = ( F ` ( ( t x. Y ) + ( ( 1 - t ) x. y ) ) ) )
108 fveq2 
 |-  ( x = Y -> ( F ` x ) = ( F ` Y ) )
109 108 oveq2d 
 |-  ( x = Y -> ( t x. ( F ` x ) ) = ( t x. ( F ` Y ) ) )
110 109 oveq1d 
 |-  ( x = Y -> ( ( t x. ( F ` x ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) = ( ( t x. ( F ` Y ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) )
111 107 110 breq12d 
 |-  ( 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 ) ) ) ) )
112 111 ralbidv 
 |-  ( 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 ) ) ) ) )
113 112 imbi2d 
 |-  ( 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 ) ) ) ) ) )
114 105 113 imbi12d 
 |-  ( 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 ) ) ) ) ) ) )
115 breq2 
 |-  ( y = X -> ( Y < y <-> Y < X ) )
116 oveq2 
 |-  ( y = X -> ( ( 1 - t ) x. y ) = ( ( 1 - t ) x. X ) )
117 116 oveq2d 
 |-  ( y = X -> ( ( t x. Y ) + ( ( 1 - t ) x. y ) ) = ( ( t x. Y ) + ( ( 1 - t ) x. X ) ) )
118 117 fveq2d 
 |-  ( y = X -> ( F ` ( ( t x. Y ) + ( ( 1 - t ) x. y ) ) ) = ( F ` ( ( t x. Y ) + ( ( 1 - t ) x. X ) ) ) )
119 fveq2 
 |-  ( y = X -> ( F ` y ) = ( F ` X ) )
120 119 oveq2d 
 |-  ( y = X -> ( ( 1 - t ) x. ( F ` y ) ) = ( ( 1 - t ) x. ( F ` X ) ) )
121 120 oveq2d 
 |-  ( y = X -> ( ( t x. ( F ` Y ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) = ( ( t x. ( F ` Y ) ) + ( ( 1 - t ) x. ( F ` X ) ) ) )
122 118 121 breq12d 
 |-  ( 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 ) ) ) ) )
123 122 ralbidv 
 |-  ( 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 ) ) ) ) )
124 123 imbi2d 
 |-  ( 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 ) ) ) ) ) )
125 115 124 imbi12d 
 |-  ( 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 ) ) ) ) ) ) )
126 114 125 51 vtocl2ga 
 |-  ( ( 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 ) ) ) ) ) )
127 102 103 104 126 syl3c 
 |-  ( ( ( 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 ) ) ) )
128 1re 
 |-  1 e. RR
129 elioore 
 |-  ( T e. ( 0 (,) 1 ) -> T e. RR )
130 resubcl 
 |-  ( ( 1 e. RR /\ T e. RR ) -> ( 1 - T ) e. RR )
131 128 129 130 sylancr 
 |-  ( T e. ( 0 (,) 1 ) -> ( 1 - T ) e. RR )
132 eliooord 
 |-  ( T e. ( 0 (,) 1 ) -> ( 0 < T /\ T < 1 ) )
133 132 simprd 
 |-  ( T e. ( 0 (,) 1 ) -> T < 1 )
134 posdif 
 |-  ( ( T e. RR /\ 1 e. RR ) -> ( T < 1 <-> 0 < ( 1 - T ) ) )
135 129 128 134 sylancl 
 |-  ( T e. ( 0 (,) 1 ) -> ( T < 1 <-> 0 < ( 1 - T ) ) )
136 133 135 mpbid 
 |-  ( T e. ( 0 (,) 1 ) -> 0 < ( 1 - T ) )
137 132 simpld 
 |-  ( T e. ( 0 (,) 1 ) -> 0 < T )
138 ltsubpos 
 |-  ( ( T e. RR /\ 1 e. RR ) -> ( 0 < T <-> ( 1 - T ) < 1 ) )
139 129 128 138 sylancl 
 |-  ( T e. ( 0 (,) 1 ) -> ( 0 < T <-> ( 1 - T ) < 1 ) )
140 137 139 mpbid 
 |-  ( T e. ( 0 (,) 1 ) -> ( 1 - T ) < 1 )
141 0xr 
 |-  0 e. RR*
142 1xr 
 |-  1 e. RR*
143 elioo2 
 |-  ( ( 0 e. RR* /\ 1 e. RR* ) -> ( ( 1 - T ) e. ( 0 (,) 1 ) <-> ( ( 1 - T ) e. RR /\ 0 < ( 1 - T ) /\ ( 1 - T ) < 1 ) ) )
144 141 142 143 mp2an 
 |-  ( ( 1 - T ) e. ( 0 (,) 1 ) <-> ( ( 1 - T ) e. RR /\ 0 < ( 1 - T ) /\ ( 1 - T ) < 1 ) )
145 131 136 140 144 syl3anbrc 
 |-  ( T e. ( 0 (,) 1 ) -> ( 1 - T ) e. ( 0 (,) 1 ) )
146 145 ad2antrl 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ ( T e. ( 0 (,) 1 ) /\ Y < X ) ) -> ( 1 - T ) e. ( 0 (,) 1 ) )
147 99 127 146 rspcdva 
 |-  ( ( ( 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 ) ) ) )
148 128 60 130 sylancr 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. RR )
149 148 10 remulcld 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 - T ) x. Y ) e. RR )
150 149 recnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 - T ) x. Y ) e. CC )
151 60 7 remulcld 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( T x. X ) e. RR )
152 151 recnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( T x. X ) e. CC )
153 nncan 
 |-  ( ( 1 e. CC /\ T e. CC ) -> ( 1 - ( 1 - T ) ) = T )
154 62 61 153 sylancr 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 1 - ( 1 - T ) ) = T )
155 154 oveq1d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 - ( 1 - T ) ) x. X ) = ( T x. X ) )
156 155 oveq2d 
 |-  ( ( 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 ) ) )
157 150 152 156 comraddd 
 |-  ( ( 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 ) ) )
158 157 adantr 
 |-  ( ( ( 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 ) ) )
159 158 fveq2d 
 |-  ( ( ( 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 ) ) ) )
160 148 75 remulcld 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 - T ) x. ( F ` Y ) ) e. RR )
161 160 recnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 - T ) x. ( F ` Y ) ) e. CC )
162 74 6 ffvelrnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( F ` X ) e. RR )
163 60 162 remulcld 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( T x. ( F ` X ) ) e. RR )
164 163 recnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( T x. ( F ` X ) ) e. CC )
165 154 oveq1d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 - ( 1 - T ) ) x. ( F ` X ) ) = ( T x. ( F ` X ) ) )
166 165 oveq2d 
 |-  ( ( 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 ) ) ) )
167 161 164 166 comraddd 
 |-  ( ( 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 ) ) ) )
168 167 adantr 
 |-  ( ( ( 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 ) ) ) )
169 147 159 168 3brtr3d 
 |-  ( ( ( 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 ) ) ) )
170 169 orcd 
 |-  ( ( ( 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 ) ) ) ) )
171 170 expr 
 |-  ( ( ( 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 ) ) ) ) ) )
172 57 90 171 3jaod 
 |-  ( ( ( 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 ) ) ) ) ) )
173 12 172 mpd 
 |-  ( ( ( 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 ) ) ) ) )
174 173 ex 
 |-  ( ( 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 ) ) ) ) ) )
175 elpri 
 |-  ( T e. { 0 , 1 } -> ( T = 0 \/ T = 1 ) )
176 76 addid2d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 0 + ( F ` Y ) ) = ( F ` Y ) )
177 162 recnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( F ` X ) e. CC )
178 177 mul02d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 0 x. ( F ` X ) ) = 0 )
179 178 78 oveq12d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 0 x. ( F ` X ) ) + ( 1 x. ( F ` Y ) ) ) = ( 0 + ( F ` Y ) ) )
180 7 recnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> X e. CC )
181 180 mul02d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 0 x. X ) = 0 )
182 181 70 oveq12d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 0 x. X ) + ( 1 x. Y ) ) = ( 0 + Y ) )
183 68 addid2d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 0 + Y ) = Y )
184 182 183 eqtrd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 0 x. X ) + ( 1 x. Y ) ) = Y )
185 184 fveq2d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( F ` ( ( 0 x. X ) + ( 1 x. Y ) ) ) = ( F ` Y ) )
186 176 179 185 3eqtr4rd 
 |-  ( ( 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 ) ) ) )
187 oveq1 
 |-  ( T = 0 -> ( T x. X ) = ( 0 x. X ) )
188 oveq2 
 |-  ( T = 0 -> ( 1 - T ) = ( 1 - 0 ) )
189 1m0e1 
 |-  ( 1 - 0 ) = 1
190 188 189 eqtrdi 
 |-  ( T = 0 -> ( 1 - T ) = 1 )
191 190 oveq1d 
 |-  ( T = 0 -> ( ( 1 - T ) x. Y ) = ( 1 x. Y ) )
192 187 191 oveq12d 
 |-  ( T = 0 -> ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) = ( ( 0 x. X ) + ( 1 x. Y ) ) )
193 192 fveq2d 
 |-  ( T = 0 -> ( F ` ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) ) = ( F ` ( ( 0 x. X ) + ( 1 x. Y ) ) ) )
194 oveq1 
 |-  ( T = 0 -> ( T x. ( F ` X ) ) = ( 0 x. ( F ` X ) ) )
195 190 oveq1d 
 |-  ( T = 0 -> ( ( 1 - T ) x. ( F ` Y ) ) = ( 1 x. ( F ` Y ) ) )
196 194 195 oveq12d 
 |-  ( T = 0 -> ( ( T x. ( F ` X ) ) + ( ( 1 - T ) x. ( F ` Y ) ) ) = ( ( 0 x. ( F ` X ) ) + ( 1 x. ( F ` Y ) ) ) )
197 193 196 eqeq12d 
 |-  ( 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 ) ) ) ) )
198 186 197 syl5ibrcom 
 |-  ( ( 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 ) ) ) ) )
199 177 addid1d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( F ` X ) + 0 ) = ( F ` X ) )
200 177 mulid2d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 1 x. ( F ` X ) ) = ( F ` X ) )
201 76 mul02d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 0 x. ( F ` Y ) ) = 0 )
202 200 201 oveq12d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 x. ( F ` X ) ) + ( 0 x. ( F ` Y ) ) ) = ( ( F ` X ) + 0 ) )
203 180 mulid2d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 1 x. X ) = X )
204 68 mul02d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 0 x. Y ) = 0 )
205 203 204 oveq12d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 x. X ) + ( 0 x. Y ) ) = ( X + 0 ) )
206 180 addid1d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( X + 0 ) = X )
207 205 206 eqtrd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 x. X ) + ( 0 x. Y ) ) = X )
208 207 fveq2d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( F ` ( ( 1 x. X ) + ( 0 x. Y ) ) ) = ( F ` X ) )
209 199 202 208 3eqtr4rd 
 |-  ( ( 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 ) ) ) )
210 oveq1 
 |-  ( T = 1 -> ( T x. X ) = ( 1 x. X ) )
211 oveq2 
 |-  ( T = 1 -> ( 1 - T ) = ( 1 - 1 ) )
212 1m1e0 
 |-  ( 1 - 1 ) = 0
213 211 212 eqtrdi 
 |-  ( T = 1 -> ( 1 - T ) = 0 )
214 213 oveq1d 
 |-  ( T = 1 -> ( ( 1 - T ) x. Y ) = ( 0 x. Y ) )
215 210 214 oveq12d 
 |-  ( T = 1 -> ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) = ( ( 1 x. X ) + ( 0 x. Y ) ) )
216 215 fveq2d 
 |-  ( T = 1 -> ( F ` ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) ) = ( F ` ( ( 1 x. X ) + ( 0 x. Y ) ) ) )
217 oveq1 
 |-  ( T = 1 -> ( T x. ( F ` X ) ) = ( 1 x. ( F ` X ) ) )
218 213 oveq1d 
 |-  ( T = 1 -> ( ( 1 - T ) x. ( F ` Y ) ) = ( 0 x. ( F ` Y ) ) )
219 217 218 oveq12d 
 |-  ( T = 1 -> ( ( T x. ( F ` X ) ) + ( ( 1 - T ) x. ( F ` Y ) ) ) = ( ( 1 x. ( F ` X ) ) + ( 0 x. ( F ` Y ) ) ) )
220 216 219 eqeq12d 
 |-  ( 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 ) ) ) ) )
221 209 220 syl5ibrcom 
 |-  ( ( 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 ) ) ) ) )
222 198 221 jaod 
 |-  ( ( 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 ) ) ) ) )
223 175 222 89 syl56 
 |-  ( ( 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 ) ) ) ) ) )
224 0le1 
 |-  0 <_ 1
225 prunioo 
 |-  ( ( 0 e. RR* /\ 1 e. RR* /\ 0 <_ 1 ) -> ( ( 0 (,) 1 ) u. { 0 , 1 } ) = ( 0 [,] 1 ) )
226 141 142 224 225 mp3an 
 |-  ( ( 0 (,) 1 ) u. { 0 , 1 } ) = ( 0 [,] 1 )
227 59 226 eleqtrrdi 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> T e. ( ( 0 (,) 1 ) u. { 0 , 1 } ) )
228 elun 
 |-  ( T e. ( ( 0 (,) 1 ) u. { 0 , 1 } ) <-> ( T e. ( 0 (,) 1 ) \/ T e. { 0 , 1 } ) )
229 227 228 sylib 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( T e. ( 0 (,) 1 ) \/ T e. { 0 , 1 } ) )
230 174 223 229 mpjaod 
 |-  ( ( 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 ) ) ) ) )
231 1 3 cvxcl 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) e. D )
232 74 231 ffvelrnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( F ` ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) ) e. RR )
233 163 160 readdcld 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. ( F ` X ) ) + ( ( 1 - T ) x. ( F ` Y ) ) ) e. RR )
234 232 233 leloed 
 |-  ( ( 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 ) ) ) ) ) )
235 230 234 mpbird 
 |-  ( ( 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 ) ) ) )