Step | Hyp | Ref
| Expression |
1 | | icchmeo.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴))) |
2 | | iitopon 24720 |
. . . . . 6
⊢ II ∈
(TopOn‘(0[,]1)) |
3 | 2 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → II ∈
(TopOn‘(0[,]1))) |
4 | | icchmeo.j |
. . . . . . . . . . 11
⊢ 𝐽 =
(TopOpen‘ℂfld) |
5 | 4 | dfii3 24724 |
. . . . . . . . . 10
⊢ II =
(𝐽 ↾t
(0[,]1)) |
6 | 5 | eqcomi 2733 |
. . . . . . . . 9
⊢ (𝐽 ↾t (0[,]1)) =
II |
7 | 6 | oveq2i 7412 |
. . . . . . . 8
⊢ (II Cn
(𝐽 ↾t
(0[,]1))) = (II Cn II) |
8 | 4 | cnfldtop 24621 |
. . . . . . . . 9
⊢ 𝐽 ∈ Top |
9 | | cnrest2r 23112 |
. . . . . . . . 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 4009 |
. . . . . . 7
⊢ (II Cn
II) ⊆ (II Cn 𝐽) |
12 | 3 | cnmptid 23486 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn II)) |
13 | 11, 12 | sselid 3972 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ (II Cn 𝐽)) |
14 | 4 | cnfldtopon 24620 |
. . . . . . . 8
⊢ 𝐽 ∈
(TopOn‘ℂ) |
15 | 14 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐽 ∈
(TopOn‘ℂ)) |
16 | | simp2 1134 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ) |
17 | 16 | recnd 11238 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℂ) |
18 | 3, 15, 17 | cnmptc 23487 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ 𝐵) ∈ (II Cn 𝐽)) |
19 | 4 | mpomulcn 24706 |
. . . . . . 7
⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) |
20 | 19 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
21 | | oveq12 7410 |
. . . . . 6
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = 𝐵) → (𝑢 · 𝑣) = (𝑥 · 𝐵)) |
22 | 3, 13, 18, 15, 15, 20, 21 | cnmpt12 23492 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ (𝑥 · 𝐵)) ∈ (II Cn 𝐽)) |
23 | | 1cnd 11205 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 1 ∈ ℂ) |
24 | 3, 15, 23 | cnmptc 23487 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ 1) ∈ (II Cn
𝐽)) |
25 | 4 | subcn 24703 |
. . . . . . . 8
⊢ −
∈ ((𝐽
×t 𝐽) Cn
𝐽) |
26 | 25 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → − ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
27 | 3, 24, 13, 26 | cnmpt12f 23491 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ (1 − 𝑥)) ∈ (II Cn 𝐽)) |
28 | | simp1 1133 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ) |
29 | 28 | recnd 11238 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℂ) |
30 | 3, 15, 29 | cnmptc 23487 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ 𝐴) ∈ (II Cn 𝐽)) |
31 | | oveq12 7410 |
. . . . . 6
⊢ ((𝑢 = (1 − 𝑥) ∧ 𝑣 = 𝐴) → (𝑢 · 𝑣) = ((1 − 𝑥) · 𝐴)) |
32 | 3, 27, 30, 15, 15, 20, 31 | cnmpt12 23492 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ ((1 − 𝑥) · 𝐴)) ∈ (II Cn 𝐽)) |
33 | 4 | addcn 24702 |
. . . . . 6
⊢ + ∈
((𝐽 ×t
𝐽) Cn 𝐽) |
34 | 33 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
35 | 3, 22, 32, 34 | cnmpt12f 23491 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴))) ∈ (II Cn 𝐽)) |
36 | 1, 35 | eqeltrid 2829 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (II Cn 𝐽)) |
37 | 1 | iccf1o 13469 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵) ∧ ◡𝐹 = (𝑦 ∈ (𝐴[,]𝐵) ↦ ((𝑦 − 𝐴) / (𝐵 − 𝐴))))) |
38 | 37 | simpld 494 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵)) |
39 | | f1of 6823 |
. . . . 5
⊢ (𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵) → 𝐹:(0[,]1)⟶(𝐴[,]𝐵)) |
40 | | frn 6714 |
. . . . 5
⊢ (𝐹:(0[,]1)⟶(𝐴[,]𝐵) → ran 𝐹 ⊆ (𝐴[,]𝐵)) |
41 | 38, 39, 40 | 3syl 18 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ran 𝐹 ⊆ (𝐴[,]𝐵)) |
42 | | iccssre 13402 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
43 | 42 | 3adant3 1129 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴[,]𝐵) ⊆ ℝ) |
44 | | ax-resscn 11162 |
. . . . 5
⊢ ℝ
⊆ ℂ |
45 | 43, 44 | sstrdi 3986 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴[,]𝐵) ⊆ ℂ) |
46 | | cnrest2 23111 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ ran 𝐹 ⊆ (𝐴[,]𝐵) ∧ (𝐴[,]𝐵) ⊆ ℂ) → (𝐹 ∈ (II Cn 𝐽) ↔ 𝐹 ∈ (II Cn (𝐽 ↾t (𝐴[,]𝐵))))) |
47 | 14, 41, 45, 46 | mp3an2i 1462 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐹 ∈ (II Cn 𝐽) ↔ 𝐹 ∈ (II Cn (𝐽 ↾t (𝐴[,]𝐵))))) |
48 | 36, 47 | mpbid 231 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (II Cn (𝐽 ↾t (𝐴[,]𝐵)))) |
49 | 37 | simprd 495 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ◡𝐹 = (𝑦 ∈ (𝐴[,]𝐵) ↦ ((𝑦 − 𝐴) / (𝐵 − 𝐴)))) |
50 | | resttopon 22986 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ (𝐴[,]𝐵) ⊆ ℂ) → (𝐽 ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵))) |
51 | 14, 45, 50 | sylancr 586 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐽 ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵))) |
52 | | cnrest2r 23112 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top → ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t (𝐴[,]𝐵))) ⊆ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
53 | 8, 52 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t (𝐴[,]𝐵))) ⊆ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽) |
54 | 51 | cnmptid 23486 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↦ 𝑦) ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t (𝐴[,]𝐵)))) |
55 | 53, 54 | sselid 3972 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↦ 𝑦) ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
56 | 51, 15, 29 | cnmptc 23487 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
57 | 51, 55, 56, 26 | cnmpt12f 23491 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 − 𝐴)) ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
58 | | difrp 13008 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈
ℝ+)) |
59 | 58 | biimp3a 1465 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐵 − 𝐴) ∈
ℝ+) |
60 | | rpcnne0 12988 |
. . . . . . 7
⊢ ((𝐵 − 𝐴) ∈ ℝ+ → ((𝐵 − 𝐴) ∈ ℂ ∧ (𝐵 − 𝐴) ≠ 0)) |
61 | 4 | divccn 24712 |
. . . . . . 7
⊢ (((𝐵 − 𝐴) ∈ ℂ ∧ (𝐵 − 𝐴) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (𝐽 Cn 𝐽)) |
62 | 59, 60, 61 | 3syl 18 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (𝐽 Cn 𝐽)) |
63 | | oveq1 7408 |
. . . . . 6
⊢ (𝑥 = (𝑦 − 𝐴) → (𝑥 / (𝐵 − 𝐴)) = ((𝑦 − 𝐴) / (𝐵 − 𝐴))) |
64 | 51, 57, 15, 62, 63 | cnmpt11 23488 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝑦 ∈ (𝐴[,]𝐵) ↦ ((𝑦 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
65 | 49, 64 | eqeltrd 2825 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽)) |
66 | | dfdm4 5885 |
. . . . . . 7
⊢ dom 𝐹 = ran ◡𝐹 |
67 | 66 | eqimss2i 4035 |
. . . . . 6
⊢ ran ◡𝐹 ⊆ dom 𝐹 |
68 | | f1odm 6827 |
. . . . . . 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 13473 |
. . . . . 6
⊢ (0[,]1)
⊆ ℂ |
72 | 71 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (0[,]1) ⊆
ℂ) |
73 | | cnrest2 23111 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ ran ◡𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆
ℂ) → (◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽) ↔ ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t
(0[,]1))))) |
74 | 14, 70, 72, 73 | mp3an2i 1462 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐽) ↔ ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t
(0[,]1))))) |
75 | 65, 74 | mpbid 231 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t
(0[,]1)))) |
76 | 5 | oveq2i 7412 |
. . 3
⊢ ((𝐽 ↾t (𝐴[,]𝐵)) Cn II) = ((𝐽 ↾t (𝐴[,]𝐵)) Cn (𝐽 ↾t
(0[,]1))) |
77 | 75, 76 | eleqtrrdi 2836 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn II)) |
78 | | ishmeo 23584 |
. 2
⊢ (𝐹 ∈ (IIHomeo(𝐽 ↾t (𝐴[,]𝐵))) ↔ (𝐹 ∈ (II Cn (𝐽 ↾t (𝐴[,]𝐵))) ∧ ◡𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn II))) |
79 | 48, 77, 78 | sylanbrc 582 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (IIHomeo(𝐽 ↾t (𝐴[,]𝐵)))) |