Metamath Proof Explorer

Theorem cvxcl

Description: Closure of a 0-1 linear combination in a convex set. (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Hypotheses cvxcl.1 
|- ( ph -> D C_ RR )
cvxcl.2 
|- ( ( ph /\ ( x e. D /\ y e. D ) ) -> ( x [,] y ) C_ D )
Assertion cvxcl 
|- ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) e. D )

Proof

Step Hyp Ref Expression
1 cvxcl.1 
 |-  ( ph -> D C_ RR )
2 cvxcl.2 
 |-  ( ( ph /\ ( x e. D /\ y e. D ) ) -> ( x [,] y ) C_ D )
3 2 ralrimivva 
 |-  ( ph -> A. x e. D A. y e. D ( x [,] y ) C_ D )
4 3 ad2antrr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ X < Y ) -> A. x e. D A. y e. D ( x [,] y ) C_ D )
5 simpr1 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> X e. D )
6 simpr2 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> Y e. D )
7 oveq1 
 |-  ( x = X -> ( x [,] y ) = ( X [,] y ) )
8 7 sseq1d 
 |-  ( x = X -> ( ( x [,] y ) C_ D <-> ( X [,] y ) C_ D ) )
9 oveq2 
 |-  ( y = Y -> ( X [,] y ) = ( X [,] Y ) )
10 9 sseq1d 
 |-  ( y = Y -> ( ( X [,] y ) C_ D <-> ( X [,] Y ) C_ D ) )
11 8 10 rspc2v 
 |-  ( ( X e. D /\ Y e. D ) -> ( A. x e. D A. y e. D ( x [,] y ) C_ D -> ( X [,] Y ) C_ D ) )
12 5 6 11 syl2anc 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( A. x e. D A. y e. D ( x [,] y ) C_ D -> ( X [,] Y ) C_ D ) )
13 12 adantr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ X < Y ) -> ( A. x e. D A. y e. D ( x [,] y ) C_ D -> ( X [,] Y ) C_ D ) )
14 4 13 mpd 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ X < Y ) -> ( X [,] Y ) C_ D )
15 ax-1cn 
 |-  1 e. CC
16 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
17 simpr3 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> T e. ( 0 [,] 1 ) )
18 16 17 sseldi 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> T e. RR )
19 18 recnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> T e. CC )
20 nncan 
 |-  ( ( 1 e. CC /\ T e. CC ) -> ( 1 - ( 1 - T ) ) = T )
21 15 19 20 sylancr 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 1 - ( 1 - T ) ) = T )
22 21 oveq1d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 - ( 1 - T ) ) x. X ) = ( T x. X ) )
23 22 oveq1d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( ( 1 - ( 1 - T ) ) x. X ) + ( ( 1 - T ) x. Y ) ) = ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) )
24 23 adantr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ X < Y ) -> ( ( ( 1 - ( 1 - T ) ) x. X ) + ( ( 1 - T ) x. Y ) ) = ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) )
25 1 adantr 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> D C_ RR )
26 25 5 sseldd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> X e. RR )
27 26 adantr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ X < Y ) -> X e. RR )
28 25 6 sseldd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> Y e. RR )
29 28 adantr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ X < Y ) -> Y e. RR )
30 simpr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ X < Y ) -> X < Y )
31 simplr3 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ X < Y ) -> T e. ( 0 [,] 1 ) )
32 iirev 
 |-  ( T e. ( 0 [,] 1 ) -> ( 1 - T ) e. ( 0 [,] 1 ) )
33 31 32 syl 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ X < Y ) -> ( 1 - T ) e. ( 0 [,] 1 ) )
34 lincmb01cmp 
 |-  ( ( ( X e. RR /\ Y e. RR /\ X < Y ) /\ ( 1 - T ) e. ( 0 [,] 1 ) ) -> ( ( ( 1 - ( 1 - T ) ) x. X ) + ( ( 1 - T ) x. Y ) ) e. ( X [,] Y ) )
35 27 29 30 33 34 syl31anc 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ X < Y ) -> ( ( ( 1 - ( 1 - T ) ) x. X ) + ( ( 1 - T ) x. Y ) ) e. ( X [,] Y ) )
36 24 35 eqeltrrd 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ X < Y ) -> ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) e. ( X [,] Y ) )
37 14 36 sseldd 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ X < Y ) -> ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) e. D )
38 oveq2 
 |-  ( X = Y -> ( T x. X ) = ( T x. Y ) )
39 38 oveq1d 
 |-  ( X = Y -> ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) = ( ( T x. Y ) + ( ( 1 - T ) x. Y ) ) )
40 pncan3 
 |-  ( ( T e. CC /\ 1 e. CC ) -> ( T + ( 1 - T ) ) = 1 )
41 19 15 40 sylancl 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( T + ( 1 - T ) ) = 1 )
42 41 oveq1d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T + ( 1 - T ) ) x. Y ) = ( 1 x. Y ) )
43 1re 
 |-  1 e. RR
44 resubcl 
 |-  ( ( 1 e. RR /\ T e. RR ) -> ( 1 - T ) e. RR )
45 43 18 44 sylancr 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. RR )
46 45 recnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. CC )
47 28 recnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> Y e. CC )
48 19 46 47 adddird 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T + ( 1 - T ) ) x. Y ) = ( ( T x. Y ) + ( ( 1 - T ) x. Y ) ) )
49 47 mulid2d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( 1 x. Y ) = Y )
50 42 48 49 3eqtr3d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. Y ) + ( ( 1 - T ) x. Y ) ) = Y )
51 39 50 sylan9eqr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ X = Y ) -> ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) = Y )
52 6 adantr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ X = Y ) -> Y e. D )
53 51 52 eqeltrd 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ X = Y ) -> ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) e. D )
54 3 ad2antrr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ Y < X ) -> A. x e. D A. y e. D ( x [,] y ) C_ D )
55 oveq1 
 |-  ( x = Y -> ( x [,] y ) = ( Y [,] y ) )
56 55 sseq1d 
 |-  ( x = Y -> ( ( x [,] y ) C_ D <-> ( Y [,] y ) C_ D ) )
57 oveq2 
 |-  ( y = X -> ( Y [,] y ) = ( Y [,] X ) )
58 57 sseq1d 
 |-  ( y = X -> ( ( Y [,] y ) C_ D <-> ( Y [,] X ) C_ D ) )
59 56 58 rspc2v 
 |-  ( ( Y e. D /\ X e. D ) -> ( A. x e. D A. y e. D ( x [,] y ) C_ D -> ( Y [,] X ) C_ D ) )
60 6 5 59 syl2anc 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( A. x e. D A. y e. D ( x [,] y ) C_ D -> ( Y [,] X ) C_ D ) )
61 60 adantr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ Y < X ) -> ( A. x e. D A. y e. D ( x [,] y ) C_ D -> ( Y [,] X ) C_ D ) )
62 54 61 mpd 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ Y < X ) -> ( Y [,] X ) C_ D )
63 26 recnd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> X e. CC )
64 19 63 mulcld 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( T x. X ) e. CC )
65 46 47 mulcld 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 - T ) x. Y ) e. CC )
66 64 65 addcomd 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) = ( ( ( 1 - T ) x. Y ) + ( T x. X ) ) )
67 66 adantr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ Y < X ) -> ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) = ( ( ( 1 - T ) x. Y ) + ( T x. X ) ) )
68 28 adantr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ Y < X ) -> Y e. RR )
69 26 adantr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ Y < X ) -> X e. RR )
70 simpr 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ Y < X ) -> Y < X )
71 simplr3 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ Y < X ) -> T e. ( 0 [,] 1 ) )
72 lincmb01cmp 
 |-  ( ( ( Y e. RR /\ X e. RR /\ Y < X ) /\ T e. ( 0 [,] 1 ) ) -> ( ( ( 1 - T ) x. Y ) + ( T x. X ) ) e. ( Y [,] X ) )
73 68 69 70 71 72 syl31anc 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ Y < X ) -> ( ( ( 1 - T ) x. Y ) + ( T x. X ) ) e. ( Y [,] X ) )
74 67 73 eqeltrd 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ Y < X ) -> ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) e. ( Y [,] X ) )
75 62 74 sseldd 
 |-  ( ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) /\ Y < X ) -> ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) e. D )
76 26 28 lttri4d 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( X < Y \/ X = Y \/ Y < X ) )
77 37 53 75 76 mpjao3dan 
 |-  ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) e. D )