| Step | Hyp | Ref
| Expression |
| 1 | | icchmeo.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴))) |
| 2 | | iitopon 24905 |
. . . . . 6
⊢ II ∈
(TopOn‘(0[,]1)) |
| 3 | 2 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → II ∈
(TopOn‘(0[,]1))) |
| 4 | | icchmeo.j |
. . . . . . . . . . 11
⊢ 𝐽 =
(TopOpen‘ℂfld) |
| 5 | 4 | dfii3 24909 |
. . . . . . . . . 10
⊢ II =
(𝐽 ↾t
(0[,]1)) |
| 6 | 5 | eqcomi 2746 |
. . . . . . . . 9
⊢ (𝐽 ↾t (0[,]1)) =
II |
| 7 | 6 | oveq2i 7442 |
. . . . . . . 8
⊢ (II Cn
(𝐽 ↾t
(0[,]1))) = (II Cn II) |
| 8 | 4 | cnfldtop 24804 |
. . . . . . . . 9
⊢ 𝐽 ∈ Top |
| 9 | | cnrest2r 23295 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top → (II Cn (𝐽 ↾t (0[,]1)))
⊆ (II Cn 𝐽)) |
| 10 | 8, 9 | ax-mp 5 |
. . . . . . . 8
⊢ (II Cn
(𝐽 ↾t
(0[,]1))) ⊆ (II Cn 𝐽) |
| 11 | 7, 10 | eqsstrri 4031 |
. . . . . . 7
⊢ (II Cn
II) ⊆ (II Cn 𝐽) |
| 12 | 3 | cnmptid 23669 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II)) |
| 13 | 11, 12 | sselid 3981 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn 𝐽)) |
| 14 | 4 | cnfldtopon 24803 |
. . . . . . . 8
⊢ 𝐽 ∈
(TopOn‘ℂ) |
| 15 | 14 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐽 ∈
(TopOn‘ℂ)) |
| 16 | | simp2 1138 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ) |
| 17 | 16 | recnd 11289 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℂ) |
| 18 | 3, 15, 17 | cnmptc 23670 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ 𝐵) ∈ (II Cn 𝐽)) |
| 19 | 4 | mpomulcn 24891 |
. . . . . . 7
⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) |
| 20 | 19 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
| 21 | | oveq12 7440 |
. . . . . 6
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = 𝐵) → (𝑢 · 𝑣) = (𝑥 · 𝐵)) |
| 22 | 3, 13, 18, 15, 15, 20, 21 | cnmpt12 23675 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ (𝑥 · 𝐵)) ∈ (II Cn 𝐽)) |
| 23 | | 1cnd 11256 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 1 ∈ ℂ) |
| 24 | 3, 15, 23 | cnmptc 23670 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ 1) ∈ (II Cn
𝐽)) |
| 25 | 4 | subcn 24888 |
. . . . . . . 8
⊢ −
∈ ((𝐽
×t 𝐽) Cn
𝐽) |
| 26 | 25 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → − ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
| 27 | 3, 24, 13, 26 | cnmpt12f 23674 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ (1 − 𝑥)) ∈ (II Cn 𝐽)) |
| 28 | | simp1 1137 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ) |
| 29 | 28 | recnd 11289 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℂ) |
| 30 | 3, 15, 29 | cnmptc 23670 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ 𝐴) ∈ (II Cn 𝐽)) |
| 31 | | oveq12 7440 |
. . . . . 6
⊢ ((𝑢 = (1 − 𝑥) ∧ 𝑣 = 𝐴) → (𝑢 · 𝑣) = ((1 − 𝑥) · 𝐴)) |
| 32 | 3, 27, 30, 15, 15, 20, 31 | cnmpt12 23675 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ ((1 − 𝑥) · 𝐴)) ∈ (II Cn 𝐽)) |
| 33 | 4 | addcn 24887 |
. . . . . 6
⊢ + ∈
((𝐽 ×t
𝐽) Cn 𝐽) |
| 34 | 33 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
| 35 | 3, 22, 32, 34 | cnmpt12f 23674 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴))) ∈ (II Cn 𝐽)) |
| 36 | 1, 35 | eqeltrid 2845 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (II Cn 𝐽)) |
| 37 | 1 | iccf1o 13536 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵) ∧ ◡𝐹 = (𝑦 ∈ (𝐴[,]𝐵) ↦ ((𝑦 − 𝐴) / (𝐵 − 𝐴))))) |
| 38 | 37 | simpld 494 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵)) |
| 39 | | f1of 6848 |
. . . . 5
⊢ (𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵) → 𝐹:(0[,]1)⟶(𝐴[,]𝐵)) |
| 40 | | frn 6743 |
. . . . 5
⊢ (𝐹:(0[,]1)⟶(𝐴[,]𝐵) → ran 𝐹 ⊆ (𝐴[,]𝐵)) |
| 41 | 38, 39, 40 | 3syl 18 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ran 𝐹 ⊆ (𝐴[,]𝐵)) |
| 42 | | iccssre 13469 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
| 43 | 42 | 3adant3 1133 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴[,]𝐵) ⊆ ℝ) |
| 44 | | ax-resscn 11212 |
. . . . 5
⊢ ℝ
⊆ ℂ |
| 45 | 43, 44 | sstrdi 3996 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴[,]𝐵) ⊆ ℂ) |
| 46 | | cnrest2 23294 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ ran 𝐹 ⊆ (𝐴[,]𝐵) ∧ (𝐴[,]𝐵) ⊆ ℂ) → (𝐹 ∈ (II Cn 𝐽) ↔ 𝐹 ∈ (II Cn (𝐽 ↾t (𝐴[,]𝐵))))) |
| 47 | 14, 41, 45, 46 | mp3an2i 1468 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐹 ∈ (II Cn 𝐽) ↔ 𝐹 ∈ (II Cn (𝐽 ↾t (𝐴[,]𝐵))))) |
| 48 | 36, 47 | mpbid 232 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (II Cn (𝐽 ↾t (𝐴[,]𝐵)))) |
| 49 | 37 | simprd 495 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ◡𝐹 = (𝑦 ∈ (𝐴[,]𝐵) ↦ ((𝑦 − 𝐴) / (𝐵 − 𝐴)))) |
| 50 | | resttopon 23169 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ (𝐴[,]𝐵) ⊆ ℂ) → (𝐽 ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵))) |
| 51 | 14, 45, 50 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐽 ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵))) |
| 52 | | cnrest2r 23295 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top → ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t (𝐴[,]𝐵))) ⊆ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
| 53 | 8, 52 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t (𝐴[,]𝐵))) ⊆ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽) |
| 54 | 51 | cnmptid 23669 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↦ 𝑦) ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t (𝐴[,]𝐵)))) |
| 55 | 53, 54 | sselid 3981 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↦ 𝑦) ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
| 56 | 51, 15, 29 | cnmptc 23670 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
| 57 | 51, 55, 56, 26 | cnmpt12f 23674 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 − 𝐴)) ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
| 58 | | difrp 13073 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈
ℝ+)) |
| 59 | 58 | biimp3a 1471 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐵 − 𝐴) ∈
ℝ+) |
| 60 | | rpcnne0 13053 |
. . . . . . 7
⊢ ((𝐵 − 𝐴) ∈ ℝ+ → ((𝐵 − 𝐴) ∈ ℂ ∧ (𝐵 − 𝐴) ≠ 0)) |
| 61 | 4 | divccn 24897 |
. . . . . . 7
⊢ (((𝐵 − 𝐴) ∈ ℂ ∧ (𝐵 − 𝐴) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (𝐽 Cn 𝐽)) |
| 62 | 59, 60, 61 | 3syl 18 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (𝐽 Cn 𝐽)) |
| 63 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥 = (𝑦 − 𝐴) → (𝑥 / (𝐵 − 𝐴)) = ((𝑦 − 𝐴) / (𝐵 − 𝐴))) |
| 64 | 51, 57, 15, 62, 63 | cnmpt11 23671 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↦ ((𝑦 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
| 65 | 49, 64 | eqeltrd 2841 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
| 66 | | dfdm4 5906 |
. . . . . . 7
⊢ dom 𝐹 = ran ◡𝐹 |
| 67 | 66 | eqimss2i 4045 |
. . . . . 6
⊢ ran ◡𝐹 ⊆ dom 𝐹 |
| 68 | | f1odm 6852 |
. . . . . . 7
⊢ (𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵) → dom 𝐹 = (0[,]1)) |
| 69 | 38, 68 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → dom 𝐹 = (0[,]1)) |
| 70 | 67, 69 | sseqtrid 4026 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ran ◡𝐹 ⊆ (0[,]1)) |
| 71 | | unitsscn 13540 |
. . . . . 6
⊢ (0[,]1)
⊆ ℂ |
| 72 | 71 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (0[,]1) ⊆
ℂ) |
| 73 | | cnrest2 23294 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ ran ◡𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆
ℂ) → (◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽) ↔ ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t
(0[,]1))))) |
| 74 | 14, 70, 72, 73 | mp3an2i 1468 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽) ↔ ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t
(0[,]1))))) |
| 75 | 65, 74 | mpbid 232 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t
(0[,]1)))) |
| 76 | 5 | oveq2i 7442 |
. . 3
⊢ ((𝐽 ↾t (𝐴[,]𝐵)) Cn II) = ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t
(0[,]1))) |
| 77 | 75, 76 | eleqtrrdi 2852 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn II)) |
| 78 | | ishmeo 23767 |
. 2
⊢ (𝐹 ∈ (IIHomeo(𝐽 ↾t (𝐴[,]𝐵))) ↔ (𝐹 ∈ (II Cn (𝐽 ↾t (𝐴[,]𝐵))) ∧ ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn II))) |
| 79 | 48, 77, 78 | sylanbrc 583 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (IIHomeo(𝐽 ↾t (𝐴[,]𝐵)))) |