Step | Hyp | Ref
| Expression |
1 | | icchmeo.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴))) |
2 | | iitopon 24242 |
. . . . . 6
⊢ II ∈
(TopOn‘(0[,]1)) |
3 | 2 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → II ∈
(TopOn‘(0[,]1))) |
4 | | icchmeo.j |
. . . . . . . . . 10
⊢ 𝐽 =
(TopOpen‘ℂfld) |
5 | 4 | dfii3 24246 |
. . . . . . . . 9
⊢ II =
(𝐽 ↾t
(0[,]1)) |
6 | 5 | oveq2i 7368 |
. . . . . . . 8
⊢ (II Cn
II) = (II Cn (𝐽
↾t (0[,]1))) |
7 | 4 | cnfldtop 24147 |
. . . . . . . . 9
⊢ 𝐽 ∈ Top |
8 | | cnrest2r 22638 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top → (II Cn (𝐽 ↾t (0[,]1)))
⊆ (II Cn 𝐽)) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . 8
⊢ (II Cn
(𝐽 ↾t
(0[,]1))) ⊆ (II Cn 𝐽) |
10 | 6, 9 | eqsstri 3978 |
. . . . . . 7
⊢ (II Cn
II) ⊆ (II Cn 𝐽) |
11 | 3 | cnmptid 23012 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II)) |
12 | 10, 11 | sselid 3942 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn 𝐽)) |
13 | 4 | cnfldtopon 24146 |
. . . . . . . 8
⊢ 𝐽 ∈
(TopOn‘ℂ) |
14 | 13 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐽 ∈
(TopOn‘ℂ)) |
15 | | simp2 1137 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ) |
16 | 15 | recnd 11183 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℂ) |
17 | 3, 14, 16 | cnmptc 23013 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ 𝐵) ∈ (II Cn 𝐽)) |
18 | 4 | mulcn 24230 |
. . . . . . 7
⊢ ·
∈ ((𝐽
×t 𝐽) Cn
𝐽) |
19 | 18 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → · ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
20 | 3, 12, 17, 19 | cnmpt12f 23017 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ (𝑥 · 𝐵)) ∈ (II Cn 𝐽)) |
21 | | 1cnd 11150 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 1 ∈ ℂ) |
22 | 3, 14, 21 | cnmptc 23013 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ 1) ∈ (II Cn
𝐽)) |
23 | 4 | subcn 24229 |
. . . . . . . 8
⊢ −
∈ ((𝐽
×t 𝐽) Cn
𝐽) |
24 | 23 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → − ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
25 | 3, 22, 12, 24 | cnmpt12f 23017 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ (1 − 𝑥)) ∈ (II Cn 𝐽)) |
26 | | simp1 1136 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ) |
27 | 26 | recnd 11183 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℂ) |
28 | 3, 14, 27 | cnmptc 23013 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ 𝐴) ∈ (II Cn 𝐽)) |
29 | 3, 25, 28, 19 | cnmpt12f 23017 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ ((1 − 𝑥) · 𝐴)) ∈ (II Cn 𝐽)) |
30 | 4 | addcn 24228 |
. . . . . 6
⊢ + ∈
((𝐽 ×t
𝐽) Cn 𝐽) |
31 | 30 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
32 | 3, 20, 29, 31 | cnmpt12f 23017 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴))) ∈ (II Cn 𝐽)) |
33 | 1, 32 | eqeltrid 2842 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (II Cn 𝐽)) |
34 | 1 | iccf1o 13413 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵) ∧ ◡𝐹 = (𝑦 ∈ (𝐴[,]𝐵) ↦ ((𝑦 − 𝐴) / (𝐵 − 𝐴))))) |
35 | 34 | simpld 495 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵)) |
36 | | f1of 6784 |
. . . . 5
⊢ (𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵) → 𝐹:(0[,]1)⟶(𝐴[,]𝐵)) |
37 | | frn 6675 |
. . . . 5
⊢ (𝐹:(0[,]1)⟶(𝐴[,]𝐵) → ran 𝐹 ⊆ (𝐴[,]𝐵)) |
38 | 35, 36, 37 | 3syl 18 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ran 𝐹 ⊆ (𝐴[,]𝐵)) |
39 | | iccssre 13346 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
40 | 39 | 3adant3 1132 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴[,]𝐵) ⊆ ℝ) |
41 | | ax-resscn 11108 |
. . . . 5
⊢ ℝ
⊆ ℂ |
42 | 40, 41 | sstrdi 3956 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴[,]𝐵) ⊆ ℂ) |
43 | | cnrest2 22637 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ ran 𝐹 ⊆ (𝐴[,]𝐵) ∧ (𝐴[,]𝐵) ⊆ ℂ) → (𝐹 ∈ (II Cn 𝐽) ↔ 𝐹 ∈ (II Cn (𝐽 ↾t (𝐴[,]𝐵))))) |
44 | 13, 38, 42, 43 | mp3an2i 1466 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐹 ∈ (II Cn 𝐽) ↔ 𝐹 ∈ (II Cn (𝐽 ↾t (𝐴[,]𝐵))))) |
45 | 33, 44 | mpbid 231 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (II Cn (𝐽 ↾t (𝐴[,]𝐵)))) |
46 | 34 | simprd 496 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ◡𝐹 = (𝑦 ∈ (𝐴[,]𝐵) ↦ ((𝑦 − 𝐴) / (𝐵 − 𝐴)))) |
47 | | resttopon 22512 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ (𝐴[,]𝐵) ⊆ ℂ) → (𝐽 ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵))) |
48 | 13, 42, 47 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐽 ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵))) |
49 | | cnrest2r 22638 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top → ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t (𝐴[,]𝐵))) ⊆ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
50 | 7, 49 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t (𝐴[,]𝐵))) ⊆ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽) |
51 | 48 | cnmptid 23012 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↦ 𝑦) ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t (𝐴[,]𝐵)))) |
52 | 50, 51 | sselid 3942 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↦ 𝑦) ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
53 | 48, 14, 27 | cnmptc 23013 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
54 | 48, 52, 53, 24 | cnmpt12f 23017 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 − 𝐴)) ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
55 | | difrp 12953 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈
ℝ+)) |
56 | 55 | biimp3a 1469 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐵 − 𝐴) ∈
ℝ+) |
57 | 56 | rpcnd 12959 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐵 − 𝐴) ∈ ℂ) |
58 | 56 | rpne0d 12962 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐵 − 𝐴) ≠ 0) |
59 | 4 | divccn 24236 |
. . . . . . 7
⊢ (((𝐵 − 𝐴) ∈ ℂ ∧ (𝐵 − 𝐴) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (𝐽 Cn 𝐽)) |
60 | 57, 58, 59 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (𝐽 Cn 𝐽)) |
61 | | oveq1 7364 |
. . . . . 6
⊢ (𝑥 = (𝑦 − 𝐴) → (𝑥 / (𝐵 − 𝐴)) = ((𝑦 − 𝐴) / (𝐵 − 𝐴))) |
62 | 48, 54, 14, 60, 61 | cnmpt11 23014 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↦ ((𝑦 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
63 | 46, 62 | eqeltrd 2838 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
64 | | dfdm4 5851 |
. . . . . . 7
⊢ dom 𝐹 = ran ◡𝐹 |
65 | 64 | eqimss2i 4003 |
. . . . . 6
⊢ ran ◡𝐹 ⊆ dom 𝐹 |
66 | | f1odm 6788 |
. . . . . . 7
⊢ (𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵) → dom 𝐹 = (0[,]1)) |
67 | 35, 66 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → dom 𝐹 = (0[,]1)) |
68 | 65, 67 | sseqtrid 3996 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ran ◡𝐹 ⊆ (0[,]1)) |
69 | | unitssre 13416 |
. . . . . . 7
⊢ (0[,]1)
⊆ ℝ |
70 | 69 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (0[,]1) ⊆
ℝ) |
71 | 70, 41 | sstrdi 3956 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (0[,]1) ⊆
ℂ) |
72 | | cnrest2 22637 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ ran ◡𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆
ℂ) → (◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽) ↔ ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t
(0[,]1))))) |
73 | 13, 68, 71, 72 | mp3an2i 1466 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽) ↔ ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t
(0[,]1))))) |
74 | 63, 73 | mpbid 231 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t
(0[,]1)))) |
75 | 5 | oveq2i 7368 |
. . 3
⊢ ((𝐽 ↾t (𝐴[,]𝐵)) Cn II) = ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t
(0[,]1))) |
76 | 74, 75 | eleqtrrdi 2849 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn II)) |
77 | | ishmeo 23110 |
. 2
⊢ (𝐹 ∈ (IIHomeo(𝐽 ↾t (𝐴[,]𝐵))) ↔ (𝐹 ∈ (II Cn (𝐽 ↾t (𝐴[,]𝐵))) ∧ ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn II))) |
78 | 45, 76, 77 | sylanbrc 583 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (IIHomeo(𝐽 ↾t (𝐴[,]𝐵)))) |