Step | Hyp | Ref
| Expression |
1 | | sconpcon 30463 |
. . 3
⊢ (𝐽 ∈ SCon → 𝐽 ∈ PCon) |
2 | | pconcon 30467 |
. . 3
⊢ (𝐽 ∈ PCon → 𝐽 ∈ Con) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝐽 ∈ SCon → 𝐽 ∈ Con) |
4 | | eqid 2610 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
5 | | eqid 2610 |
. . . . . . 7
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
6 | 4, 5 | rerest 22415 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ →
((TopOpen‘ℂfld) ↾t 𝐴) = ((topGen‘ran (,))
↾t 𝐴)) |
7 | | rescon.1 |
. . . . . 6
⊢ 𝐽 = ((topGen‘ran (,))
↾t 𝐴) |
8 | 6, 7 | syl6eqr 2662 |
. . . . 5
⊢ (𝐴 ⊆ ℝ →
((TopOpen‘ℂfld) ↾t 𝐴) = 𝐽) |
9 | 8 | adantr 480 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) →
((TopOpen‘ℂfld) ↾t 𝐴) = 𝐽) |
10 | | simpl 472 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) → 𝐴 ⊆
ℝ) |
11 | | ax-resscn 9872 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
12 | 10, 11 | syl6ss 3580 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) → 𝐴 ⊆
ℂ) |
13 | | df-3an 1033 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑡 ∈ (0[,]1)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑡 ∈ (0[,]1))) |
14 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑥 → (𝑡 · 𝑧) = (𝑡 · 𝑥)) |
15 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑦 → ((1 − 𝑡) · 𝑤) = ((1 − 𝑡) · 𝑦)) |
16 | 14, 15 | oveqan12d 6568 |
. . . . . . . . . . 11
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → ((𝑡 · 𝑧) + ((1 − 𝑡) · 𝑤)) = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) |
17 | 16 | eleq1d 2672 |
. . . . . . . . . 10
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (((𝑡 · 𝑧) + ((1 − 𝑡) · 𝑤)) ∈ 𝐴 ↔ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝐴)) |
18 | 17 | ralbidv 2969 |
. . . . . . . . 9
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (∀𝑡 ∈ (0[,]1)((𝑡 · 𝑧) + ((1 − 𝑡) · 𝑤)) ∈ 𝐴 ↔ ∀𝑡 ∈ (0[,]1)((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝐴)) |
19 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → (𝑡 · 𝑧) = (𝑡 · 𝑦)) |
20 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → ((1 − 𝑡) · 𝑤) = ((1 − 𝑡) · 𝑥)) |
21 | 19, 20 | oveqan12d 6568 |
. . . . . . . . . . 11
⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → ((𝑡 · 𝑧) + ((1 − 𝑡) · 𝑤)) = ((𝑡 · 𝑦) + ((1 − 𝑡) · 𝑥))) |
22 | 21 | eleq1d 2672 |
. . . . . . . . . 10
⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → (((𝑡 · 𝑧) + ((1 − 𝑡) · 𝑤)) ∈ 𝐴 ↔ ((𝑡 · 𝑦) + ((1 − 𝑡) · 𝑥)) ∈ 𝐴)) |
23 | 22 | ralbidv 2969 |
. . . . . . . . 9
⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → (∀𝑡 ∈ (0[,]1)((𝑡 · 𝑧) + ((1 − 𝑡) · 𝑤)) ∈ 𝐴 ↔ ∀𝑡 ∈ (0[,]1)((𝑡 · 𝑦) + ((1 − 𝑡) · 𝑥)) ∈ 𝐴)) |
24 | | unitssre 12190 |
. . . . . . . . . . . . . . . . 17
⊢ (0[,]1)
⊆ ℝ |
25 | 24, 11 | sstri 3577 |
. . . . . . . . . . . . . . . 16
⊢ (0[,]1)
⊆ ℂ |
26 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → 𝑠 ∈ (0[,]1)) |
27 | 25, 26 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → 𝑠 ∈ ℂ) |
28 | 12 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) → 𝐴 ⊆ ℂ) |
29 | | simpr2 1061 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) → 𝑦 ∈ 𝐴) |
30 | 28, 29 | sseldd 3569 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) → 𝑦 ∈ ℂ) |
31 | 30 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → 𝑦 ∈ ℂ) |
32 | 27, 31 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → (𝑠 · 𝑦) ∈ ℂ) |
33 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
34 | | subcl 10159 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ 𝑠
∈ ℂ) → (1 − 𝑠) ∈ ℂ) |
35 | 33, 27, 34 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → (1 − 𝑠) ∈
ℂ) |
36 | | simpr1 1060 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) → 𝑥 ∈ 𝐴) |
37 | 28, 36 | sseldd 3569 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) → 𝑥 ∈ ℂ) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → 𝑥 ∈ ℂ) |
39 | 35, 38 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) · 𝑥) ∈ ℂ) |
40 | 32, 39 | addcomd 10117 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → ((𝑠 · 𝑦) + ((1 − 𝑠) · 𝑥)) = (((1 − 𝑠) · 𝑥) + (𝑠 · 𝑦))) |
41 | | nncan 10189 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ 𝑠
∈ ℂ) → (1 − (1 − 𝑠)) = 𝑠) |
42 | 33, 27, 41 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → (1 − (1 −
𝑠)) = 𝑠) |
43 | 42 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → ((1 − (1
− 𝑠)) · 𝑦) = (𝑠 · 𝑦)) |
44 | 43 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → (((1 − 𝑠) · 𝑥) + ((1 − (1 − 𝑠)) · 𝑦)) = (((1 − 𝑠) · 𝑥) + (𝑠 · 𝑦))) |
45 | 40, 44 | eqtr4d 2647 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → ((𝑠 · 𝑦) + ((1 − 𝑠) · 𝑥)) = (((1 − 𝑠) · 𝑥) + ((1 − (1 − 𝑠)) · 𝑦))) |
46 | | iirev 22536 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ (0[,]1) → (1
− 𝑠) ∈
(0[,]1)) |
47 | 46 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → (1 − 𝑠) ∈
(0[,]1)) |
48 | 7 | eleq1i 2679 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐽 ∈ Con ↔
((topGen‘ran (,)) ↾t 𝐴) ∈ Con) |
49 | | reconn 22439 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ⊆ ℝ →
(((topGen‘ran (,)) ↾t 𝐴) ∈ Con ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴)) |
50 | 48, 49 | syl5bb 271 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ⊆ ℝ → (𝐽 ∈ Con ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴)) |
51 | 50 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) →
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) |
52 | 51 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) |
53 | 52 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥[,]𝑦) ⊆ 𝐴) |
54 | 53 | anasss 677 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥[,]𝑦) ⊆ 𝐴) |
55 | 54 | 3adantr3 1215 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) → (𝑥[,]𝑦) ⊆ 𝐴) |
56 | 55 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → (𝑥[,]𝑦) ⊆ 𝐴) |
57 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ (0[,]1)) |
58 | 24, 57 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℝ) |
59 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → 𝐴 ⊆ ℝ) |
60 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → 𝑥 ∈ 𝐴) |
61 | 59, 60 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → 𝑥 ∈ ℝ) |
62 | 58, 61 | remulcld 9949 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → (𝑡 · 𝑥) ∈ ℝ) |
63 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ |
64 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℝ ∧ 𝑡
∈ ℝ) → (1 − 𝑡) ∈ ℝ) |
65 | 63, 58, 64 | sylancr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → (1 − 𝑡) ∈
ℝ) |
66 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → 𝑦 ∈ 𝐴) |
67 | 59, 66 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → 𝑦 ∈ ℝ) |
68 | 65, 67 | remulcld 9949 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → ((1 − 𝑡) · 𝑦) ∈ ℝ) |
69 | 62, 68 | readdcld 9948 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ) |
70 | 58 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℂ) |
71 | | pncan3 10168 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑡 + (1
− 𝑡)) =
1) |
72 | 70, 33, 71 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → (𝑡 + (1 − 𝑡)) = 1) |
73 | 72 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 + (1 − 𝑡)) · 𝑥) = (1 · 𝑥)) |
74 | 65 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → (1 − 𝑡) ∈
ℂ) |
75 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → 𝑥 ∈ ℂ) |
76 | 70, 74, 75 | adddird 9944 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 + (1 − 𝑡)) · 𝑥) = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑥))) |
77 | 75 | mulid2d 9937 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → (1 · 𝑥) = 𝑥) |
78 | 73, 76, 77 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑥)) = 𝑥) |
79 | 65, 61 | remulcld 9949 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → ((1 − 𝑡) · 𝑥) ∈ ℝ) |
80 | | 0re 9919 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
ℝ |
81 | 80, 63 | elicc2i 12110 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤
𝑡 ∧ 𝑡 ≤ 1)) |
82 | 57, 81 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1)) |
83 | 82 | simp3d 1068 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ≤ 1) |
84 | | subge0 10420 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℝ ∧ 𝑡
∈ ℝ) → (0 ≤ (1 − 𝑡) ↔ 𝑡 ≤ 1)) |
85 | 63, 58, 84 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → (0 ≤ (1 −
𝑡) ↔ 𝑡 ≤ 1)) |
86 | 83, 85 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → 0 ≤ (1 −
𝑡)) |
87 | | simplr3 1098 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → 𝑥 ≤ 𝑦) |
88 | 61, 67, 65, 86, 87 | lemul2ad 10843 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → ((1 − 𝑡) · 𝑥) ≤ ((1 − 𝑡) · 𝑦)) |
89 | 79, 68, 62, 88 | leadd2dd 10521 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑥)) ≤ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) |
90 | 78, 89 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → 𝑥 ≤ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) |
91 | 58, 67 | remulcld 9949 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → (𝑡 · 𝑦) ∈ ℝ) |
92 | 82 | simp2d 1067 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → 0 ≤ 𝑡) |
93 | 61, 67, 58, 92, 87 | lemul2ad 10843 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → (𝑡 · 𝑥) ≤ (𝑡 · 𝑦)) |
94 | 62, 91, 68, 93 | leadd1dd 10520 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ≤ ((𝑡 · 𝑦) + ((1 − 𝑡) · 𝑦))) |
95 | 72 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 + (1 − 𝑡)) · 𝑦) = (1 · 𝑦)) |
96 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → 𝑦 ∈ ℂ) |
97 | 70, 74, 96 | adddird 9944 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 + (1 − 𝑡)) · 𝑦) = ((𝑡 · 𝑦) + ((1 − 𝑡) · 𝑦))) |
98 | 96 | mulid2d 9937 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → (1 · 𝑦) = 𝑦) |
99 | 95, 97, 98 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑦) + ((1 − 𝑡) · 𝑦)) = 𝑦) |
100 | 94, 99 | breqtrd 4609 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ≤ 𝑦) |
101 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ (𝑥[,]𝑦) ↔ (((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ ∧ 𝑥 ≤ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∧ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ≤ 𝑦))) |
102 | 61, 67, 101 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → (((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ (𝑥[,]𝑦) ↔ (((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ ∧ 𝑥 ≤ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∧ ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ≤ 𝑦))) |
103 | 69, 90, 100, 102 | mpbir3and 1238 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ (𝑥[,]𝑦)) |
104 | 56, 103 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝐴) |
105 | 104 | ralrimiva 2949 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) → ∀𝑡 ∈ (0[,]1)((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝐴) |
106 | 105 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → ∀𝑡 ∈ (0[,]1)((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝐴) |
107 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (1 − 𝑠) → (𝑡 · 𝑥) = ((1 − 𝑠) · 𝑥)) |
108 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (1 − 𝑠) → (1 − 𝑡) = (1 − (1 − 𝑠))) |
109 | 108 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (1 − 𝑠) → ((1 − 𝑡) · 𝑦) = ((1 − (1 − 𝑠)) · 𝑦)) |
110 | 107, 109 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (1 − 𝑠) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) = (((1 − 𝑠) · 𝑥) + ((1 − (1 − 𝑠)) · 𝑦))) |
111 | 110 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (1 − 𝑠) → (((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝐴 ↔ (((1 − 𝑠) · 𝑥) + ((1 − (1 − 𝑠)) · 𝑦)) ∈ 𝐴)) |
112 | 111 | rspcv 3278 |
. . . . . . . . . . . . 13
⊢ ((1
− 𝑠) ∈ (0[,]1)
→ (∀𝑡 ∈
(0[,]1)((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝐴 → (((1 − 𝑠) · 𝑥) + ((1 − (1 − 𝑠)) · 𝑦)) ∈ 𝐴)) |
113 | 47, 106, 112 | sylc 63 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → (((1 − 𝑠) · 𝑥) + ((1 − (1 − 𝑠)) · 𝑦)) ∈ 𝐴) |
114 | 45, 113 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) ∧ 𝑠 ∈ (0[,]1)) → ((𝑠 · 𝑦) + ((1 − 𝑠) · 𝑥)) ∈ 𝐴) |
115 | 114 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) → ∀𝑠 ∈ (0[,]1)((𝑠 · 𝑦) + ((1 − 𝑠) · 𝑥)) ∈ 𝐴) |
116 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑡 → (𝑠 · 𝑦) = (𝑡 · 𝑦)) |
117 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑡 → (1 − 𝑠) = (1 − 𝑡)) |
118 | 117 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑡 → ((1 − 𝑠) · 𝑥) = ((1 − 𝑡) · 𝑥)) |
119 | 116, 118 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑡 → ((𝑠 · 𝑦) + ((1 − 𝑠) · 𝑥)) = ((𝑡 · 𝑦) + ((1 − 𝑡) · 𝑥))) |
120 | 119 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑡 → (((𝑠 · 𝑦) + ((1 − 𝑠) · 𝑥)) ∈ 𝐴 ↔ ((𝑡 · 𝑦) + ((1 − 𝑡) · 𝑥)) ∈ 𝐴)) |
121 | 120 | cbvralv 3147 |
. . . . . . . . . 10
⊢
(∀𝑠 ∈
(0[,]1)((𝑠 · 𝑦) + ((1 − 𝑠) · 𝑥)) ∈ 𝐴 ↔ ∀𝑡 ∈ (0[,]1)((𝑡 · 𝑦) + ((1 − 𝑡) · 𝑥)) ∈ 𝐴) |
122 | 115, 121 | sylib 207 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)) → ∀𝑡 ∈ (0[,]1)((𝑡 · 𝑦) + ((1 − 𝑡) · 𝑥)) ∈ 𝐴) |
123 | 18, 23, 10, 122, 105 | wloglei 10439 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ∀𝑡 ∈ (0[,]1)((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝐴) |
124 | 123 | r19.21bi 2916 |
. . . . . . 7
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝐴) |
125 | 124 | anasss 677 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝐴) |
126 | 13, 125 | sylan2b 491 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝐴) |
127 | | eqid 2610 |
. . . . 5
⊢
((TopOpen‘ℂfld) ↾t 𝐴) =
((TopOpen‘ℂfld) ↾t 𝐴) |
128 | 12, 126, 4, 127 | cvxscon 30479 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) →
((TopOpen‘ℂfld) ↾t 𝐴) ∈ SCon) |
129 | 9, 128 | eqeltrrd 2689 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐽 ∈ Con) → 𝐽 ∈ SCon) |
130 | 129 | ex 449 |
. 2
⊢ (𝐴 ⊆ ℝ → (𝐽 ∈ Con → 𝐽 ∈ SCon)) |
131 | 3, 130 | impbid2 215 |
1
⊢ (𝐴 ⊆ ℝ → (𝐽 ∈ SCon ↔ 𝐽 ∈ Con)) |