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→xy⊆D
Assertion cvxcl ⊢φ∧X∈D∧Y∈D∧T∈01→T⁢X+1−T⁢Y∈D

Proof

Step Hyp Ref Expression
1 cvxcl.1 ⊢φ→D⊆ℝ
2 cvxcl.2 ⊢φ∧x∈D∧y∈D→xy⊆D
3 2 ralrimivva ⊢φ→∀x∈D∀y∈Dxy⊆D
4 3 ad2antrr ⊢φ∧X∈D∧Y∈D∧T∈01∧X<Y→∀x∈D∀y∈Dxy⊆D
5 simpr1 ⊢φ∧X∈D∧Y∈D∧T∈01→X∈D
6 simpr2 ⊢φ∧X∈D∧Y∈D∧T∈01→Y∈D
7 oveq1 ⊢x=X→xy=Xy
8 7 sseq1d ⊢x=X→xy⊆D↔Xy⊆D
9 oveq2 ⊢y=Y→Xy=XY
10 9 sseq1d ⊢y=Y→Xy⊆D↔XY⊆D
11 8 10 rspc2v ⊢X∈D∧Y∈D→∀x∈D∀y∈Dxy⊆D→XY⊆D
12 5 6 11 syl2anc ⊢φ∧X∈D∧Y∈D∧T∈01→∀x∈D∀y∈Dxy⊆D→XY⊆D
13 12 adantr ⊢φ∧X∈D∧Y∈D∧T∈01∧X<Y→∀x∈D∀y∈Dxy⊆D→XY⊆D
14 4 13 mpd ⊢φ∧X∈D∧Y∈D∧T∈01∧X<Y→XY⊆D
15 ax-1cn ⊢1∈ℂ
16 unitssre ⊢01⊆ℝ
17 simpr3 ⊢φ∧X∈D∧Y∈D∧T∈01→T∈01
18 16 17 sselid ⊢φ∧X∈D∧Y∈D∧T∈01→T∈ℝ
19 18 recnd ⊢φ∧X∈D∧Y∈D∧T∈01→T∈ℂ
20 nncan ⊢1∈ℂ∧T∈ℂ→1−1−T=T
21 15 19 20 sylancr ⊢φ∧X∈D∧Y∈D∧T∈01→1−1−T=T
22 21 oveq1d ⊢φ∧X∈D∧Y∈D∧T∈01→1−1−T⁢X=T⁢X
23 22 oveq1d ⊢φ∧X∈D∧Y∈D∧T∈01→1−1−T⁢X+1−T⁢Y=T⁢X+1−T⁢Y
24 23 adantr ⊢φ∧X∈D∧Y∈D∧T∈01∧X<Y→1−1−T⁢X+1−T⁢Y=T⁢X+1−T⁢Y
25 1 adantr ⊢φ∧X∈D∧Y∈D∧T∈01→D⊆ℝ
26 25 5 sseldd ⊢φ∧X∈D∧Y∈D∧T∈01→X∈ℝ
27 26 adantr ⊢φ∧X∈D∧Y∈D∧T∈01∧X<Y→X∈ℝ
28 25 6 sseldd ⊢φ∧X∈D∧Y∈D∧T∈01→Y∈ℝ
29 28 adantr ⊢φ∧X∈D∧Y∈D∧T∈01∧X<Y→Y∈ℝ
30 simpr ⊢φ∧X∈D∧Y∈D∧T∈01∧X<Y→X<Y
31 simplr3 ⊢φ∧X∈D∧Y∈D∧T∈01∧X<Y→T∈01
32 iirev ⊢T∈01→1−T∈01
33 31 32 syl ⊢φ∧X∈D∧Y∈D∧T∈01∧X<Y→1−T∈01
34 lincmb01cmp ⊢X∈ℝ∧Y∈ℝ∧X<Y∧1−T∈01→1−1−T⁢X+1−T⁢Y∈XY
35 27 29 30 33 34 syl31anc ⊢φ∧X∈D∧Y∈D∧T∈01∧X<Y→1−1−T⁢X+1−T⁢Y∈XY
36 24 35 eqeltrrd ⊢φ∧X∈D∧Y∈D∧T∈01∧X<Y→T⁢X+1−T⁢Y∈XY
37 14 36 sseldd ⊢φ∧X∈D∧Y∈D∧T∈01∧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∈01→T+1-T=1
42 41 oveq1d ⊢φ∧X∈D∧Y∈D∧T∈01→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∈01→1−T∈ℝ
46 45 recnd ⊢φ∧X∈D∧Y∈D∧T∈01→1−T∈ℂ
47 28 recnd ⊢φ∧X∈D∧Y∈D∧T∈01→Y∈ℂ
48 19 46 47 adddird ⊢φ∧X∈D∧Y∈D∧T∈01→T+1-T⁢Y=T⁢Y+1−T⁢Y
49 47 mullidd ⊢φ∧X∈D∧Y∈D∧T∈01→1⁢Y=Y
50 42 48 49 3eqtr3d ⊢φ∧X∈D∧Y∈D∧T∈01→T⁢Y+1−T⁢Y=Y
51 39 50 sylan9eqr ⊢φ∧X∈D∧Y∈D∧T∈01∧X=Y→T⁢X+1−T⁢Y=Y
52 6 adantr ⊢φ∧X∈D∧Y∈D∧T∈01∧X=Y→Y∈D
53 51 52 eqeltrd ⊢φ∧X∈D∧Y∈D∧T∈01∧X=Y→T⁢X+1−T⁢Y∈D
54 3 ad2antrr ⊢φ∧X∈D∧Y∈D∧T∈01∧Y<X→∀x∈D∀y∈Dxy⊆D
55 oveq1 ⊢x=Y→xy=Yy
56 55 sseq1d ⊢x=Y→xy⊆D↔Yy⊆D
57 oveq2 ⊢y=X→Yy=YX
58 57 sseq1d ⊢y=X→Yy⊆D↔YX⊆D
59 56 58 rspc2v ⊢Y∈D∧X∈D→∀x∈D∀y∈Dxy⊆D→YX⊆D
60 6 5 59 syl2anc ⊢φ∧X∈D∧Y∈D∧T∈01→∀x∈D∀y∈Dxy⊆D→YX⊆D
61 60 adantr ⊢φ∧X∈D∧Y∈D∧T∈01∧Y<X→∀x∈D∀y∈Dxy⊆D→YX⊆D
62 54 61 mpd ⊢φ∧X∈D∧Y∈D∧T∈01∧Y<X→YX⊆D
63 26 recnd ⊢φ∧X∈D∧Y∈D∧T∈01→X∈ℂ
64 19 63 mulcld ⊢φ∧X∈D∧Y∈D∧T∈01→T⁢X∈ℂ
65 46 47 mulcld ⊢φ∧X∈D∧Y∈D∧T∈01→1−T⁢Y∈ℂ
66 64 65 addcomd ⊢φ∧X∈D∧Y∈D∧T∈01→T⁢X+1−T⁢Y=1−T⁢Y+T⁢X
67 66 adantr ⊢φ∧X∈D∧Y∈D∧T∈01∧Y<X→T⁢X+1−T⁢Y=1−T⁢Y+T⁢X
68 28 adantr ⊢φ∧X∈D∧Y∈D∧T∈01∧Y<X→Y∈ℝ
69 26 adantr ⊢φ∧X∈D∧Y∈D∧T∈01∧Y<X→X∈ℝ
70 simpr ⊢φ∧X∈D∧Y∈D∧T∈01∧Y<X→Y<X
71 simplr3 ⊢φ∧X∈D∧Y∈D∧T∈01∧Y<X→T∈01
72 lincmb01cmp ⊢Y∈ℝ∧X∈ℝ∧Y<X∧T∈01→1−T⁢Y+T⁢X∈YX
73 68 69 70 71 72 syl31anc ⊢φ∧X∈D∧Y∈D∧T∈01∧Y<X→1−T⁢Y+T⁢X∈YX
74 67 73 eqeltrd ⊢φ∧X∈D∧Y∈D∧T∈01∧Y<X→T⁢X+1−T⁢Y∈YX
75 62 74 sseldd ⊢φ∧X∈D∧Y∈D∧T∈01∧Y<X→T⁢X+1−T⁢Y∈D
76 26 28 lttri4d ⊢φ∧X∈D∧Y∈D∧T∈01→X<Y∨X=Y∨Y<X
77 37 53 75 76 mpjao3dan ⊢φ∧X∈D∧Y∈D∧T∈01→T⁢X+1−T⁢Y∈D