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 sselid ⊢ φ ∧ 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