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 ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
cvxcl.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 )
Assertion cvxcl ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 cvxcl.1 ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
2 cvxcl.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 )
3 2 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 )
4 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 )
5 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑋 ∈ 𝐷 )
6 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑌 ∈ 𝐷 )
7 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 [,] 𝑦 ) = ( 𝑋 [,] 𝑦 ) )
8 7 sseq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 ↔ ( 𝑋 [,] 𝑦 ) ⊆ 𝐷 ) )
9 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 [,] 𝑦 ) = ( 𝑋 [,] 𝑌 ) )
10 9 sseq1d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 [,] 𝑦 ) ⊆ 𝐷 ↔ ( 𝑋 [,] 𝑌 ) ⊆ 𝐷 ) )
11 8 10 rspc2v ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 → ( 𝑋 [,] 𝑌 ) ⊆ 𝐷 ) )
12 5 6 11 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 → ( 𝑋 [,] 𝑌 ) ⊆ 𝐷 ) )
13 12 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 → ( 𝑋 [,] 𝑌 ) ⊆ 𝐷 ) )
14 4 13 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 [,] 𝑌 ) ⊆ 𝐷 )
15 ax-1cn ⊢ 1 ∈ ℂ
16 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
17 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ( 0 [,] 1 ) )
18 16 17 sselid ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ℝ )
19 18 recnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ℂ )
20 nncan ⊢ ( ( 1 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 1 − ( 1 − 𝑇 ) ) = 𝑇 )
21 15 19 20 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 1 − ( 1 − 𝑇 ) ) = 𝑇 )
22 21 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) = ( 𝑇 · 𝑋 ) )
23 22 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) )
24 23 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) )
25 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝐷 ⊆ ℝ )
26 25 5 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑋 ∈ ℝ )
27 26 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑋 ∈ ℝ )
28 25 6 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑌 ∈ ℝ )
29 28 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑌 ∈ ℝ )
30 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑋 < 𝑌 )
31 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑇 ∈ ( 0 [,] 1 ) )
32 iirev ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → ( 1 − 𝑇 ) ∈ ( 0 [,] 1 ) )
33 31 32 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ( 1 − 𝑇 ) ∈ ( 0 [,] 1 ) )
34 lincmb01cmp ⊢ ( ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ 𝑋 < 𝑌 ) ∧ ( 1 − 𝑇 ) ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ ( 𝑋 [,] 𝑌 ) )
35 27 29 30 33 34 syl31anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ ( 𝑋 [,] 𝑌 ) )
36 24 35 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ ( 𝑋 [,] 𝑌 ) )
37 14 36 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ 𝐷 )
38 oveq2 ⊢ ( 𝑋 = 𝑌 → ( 𝑇 · 𝑋 ) = ( 𝑇 · 𝑌 ) )
39 38 oveq1d ⊢ ( 𝑋 = 𝑌 → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = ( ( 𝑇 · 𝑌 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) )
40 pncan3 ⊢ ( ( 𝑇 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑇 + ( 1 − 𝑇 ) ) = 1 )
41 19 15 40 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 + ( 1 − 𝑇 ) ) = 1 )
42 41 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 + ( 1 − 𝑇 ) ) · 𝑌 ) = ( 1 · 𝑌 ) )
43 1re ⊢ 1 ∈ ℝ
44 resubcl ⊢ ( ( 1 ∈ ℝ ∧ 𝑇 ∈ ℝ ) → ( 1 − 𝑇 ) ∈ ℝ )
45 43 18 44 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑇 ) ∈ ℝ )
46 45 recnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑇 ) ∈ ℂ )
47 28 recnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑌 ∈ ℂ )
48 19 46 47 adddird ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 + ( 1 − 𝑇 ) ) · 𝑌 ) = ( ( 𝑇 · 𝑌 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) )
49 47 mulid2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 1 · 𝑌 ) = 𝑌 )
50 42 48 49 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · 𝑌 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = 𝑌 )
51 39 50 sylan9eqr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 = 𝑌 ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = 𝑌 )
52 6 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 = 𝑌 ) → 𝑌 ∈ 𝐷 )
53 51 52 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 = 𝑌 ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ 𝐷 )
54 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 )
55 oveq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 [,] 𝑦 ) = ( 𝑌 [,] 𝑦 ) )
56 55 sseq1d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 ↔ ( 𝑌 [,] 𝑦 ) ⊆ 𝐷 ) )
57 oveq2 ⊢ ( 𝑦 = 𝑋 → ( 𝑌 [,] 𝑦 ) = ( 𝑌 [,] 𝑋 ) )
58 57 sseq1d ⊢ ( 𝑦 = 𝑋 → ( ( 𝑌 [,] 𝑦 ) ⊆ 𝐷 ↔ ( 𝑌 [,] 𝑋 ) ⊆ 𝐷 ) )
59 56 58 rspc2v ⊢ ( ( 𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 → ( 𝑌 [,] 𝑋 ) ⊆ 𝐷 ) )
60 6 5 59 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 → ( 𝑌 [,] 𝑋 ) ⊆ 𝐷 ) )
61 60 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 → ( 𝑌 [,] 𝑋 ) ⊆ 𝐷 ) )
62 54 61 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → ( 𝑌 [,] 𝑋 ) ⊆ 𝐷 )
63 26 recnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑋 ∈ ℂ )
64 19 63 mulcld ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 · 𝑋 ) ∈ ℂ )
65 46 47 mulcld ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 1 − 𝑇 ) · 𝑌 ) ∈ ℂ )
66 64 65 addcomd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( 𝑇 · 𝑋 ) ) )
67 66 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( 𝑇 · 𝑋 ) ) )
68 28 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → 𝑌 ∈ ℝ )
69 26 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → 𝑋 ∈ ℝ )
70 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → 𝑌 < 𝑋 )
71 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → 𝑇 ∈ ( 0 [,] 1 ) )
72 lincmb01cmp ⊢ ( ( ( 𝑌 ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ 𝑌 < 𝑋 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( 𝑇 · 𝑋 ) ) ∈ ( 𝑌 [,] 𝑋 ) )
73 68 69 70 71 72 syl31anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( 𝑇 · 𝑋 ) ) ∈ ( 𝑌 [,] 𝑋 ) )
74 67 73 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ ( 𝑌 [,] 𝑋 ) )
75 62 74 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ 𝐷 )
76 26 28 lttri4d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ∨ 𝑌 < 𝑋 ) )
77 37 53 75 76 mpjao3dan ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ 𝐷 )