# 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 ${⊢}{\phi }\to {D}\subseteq ℝ$
cvxcl.2 ${⊢}\left({\phi }\wedge \left({x}\in {D}\wedge {y}\in {D}\right)\right)\to \left[{x},{y}\right]\subseteq {D}$
Assertion cvxcl ${⊢}\left({\phi }\wedge \left({X}\in {D}\wedge {Y}\in {D}\wedge {T}\in \left[0,1\right]\right)\right)\to {T}{X}+\left(1-{T}\right){Y}\in {D}$

### Proof

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