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 φ D
cvxcl.2 φ x D y D x y D
Assertion cvxcl φ X D Y D T 0 1 T X + 1 T Y D

Proof

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