Metamath Proof Explorer

Theorem icchmeo

Description: The natural bijection from [ 0 , 1 ] to an arbitrary nontrivial closed interval [ A , B ] is a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypotheses icchmeo.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
icchmeo.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) )
Assertion icchmeo ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐹 ∈ ( II Homeo ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 icchmeo.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 icchmeo.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) )
3 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
4 3 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
5 1 dfii3 ⊢ II = ( 𝐽 ↾t ( 0 [,] 1 ) )
6 5 eqcomi ⊢ ( 𝐽 ↾t ( 0 [,] 1 ) ) = II
7 6 oveq2i ⊢ ( II Cn ( 𝐽 ↾t ( 0 [,] 1 ) ) ) = ( II Cn II )
8 1 cnfldtop ⊢ 𝐽 ∈ Top
9 cnrest2r ⊢ ( 𝐽 ∈ Top → ( II Cn ( 𝐽 ↾t ( 0 [,] 1 ) ) ) ⊆ ( II Cn 𝐽 ) )
10 8 9 ax-mp ⊢ ( II Cn ( 𝐽 ↾t ( 0 [,] 1 ) ) ) ⊆ ( II Cn 𝐽 )
11 7 10 eqsstrri ⊢ ( II Cn II ) ⊆ ( II Cn 𝐽 )
12 4 cnmptid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 𝑥 ) ∈ ( II Cn II ) )
13 11 12 sselid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 𝑥 ) ∈ ( II Cn 𝐽 ) )
14 1 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
15 14 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐽 ∈ ( TopOn ‘ ℂ ) )
16 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ )
17 16 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℂ )
18 4 15 17 cnmptc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 𝐵 ) ∈ ( II Cn 𝐽 ) )
19 1 mpomulcn ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
20 19 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
21 oveq12 ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝐵 ) → ( 𝑢 · 𝑣 ) = ( 𝑥 · 𝐵 ) )
22 4 13 18 15 15 20 21 cnmpt12 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝐵 ) ) ∈ ( II Cn 𝐽 ) )
23 1cnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 1 ∈ ℂ )
24 4 15 23 cnmptc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 1 ) ∈ ( II Cn 𝐽 ) )
25 1 subcn ⊢ − ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
26 25 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → − ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
27 4 24 13 26 cnmpt12f ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 1 − 𝑥 ) ) ∈ ( II Cn 𝐽 ) )
28 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ )
29 28 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℂ )
30 4 15 29 cnmptc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 𝐴 ) ∈ ( II Cn 𝐽 ) )
31 oveq12 ⊢ ( ( 𝑢 = ( 1 − 𝑥 ) ∧ 𝑣 = 𝐴 ) → ( 𝑢 · 𝑣 ) = ( ( 1 − 𝑥 ) · 𝐴 ) )
32 4 27 30 15 15 20 31 cnmpt12 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 1 − 𝑥 ) · 𝐴 ) ) ∈ ( II Cn 𝐽 ) )
33 1 addcn ⊢ + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
34 33 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
35 4 22 32 34 cnmpt12f ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) ) ∈ ( II Cn 𝐽 ) )
36 2 35 eqeltrid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐹 ∈ ( II Cn 𝐽 ) )
37 2 iccf1o ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 𝐴 [,] 𝐵 ) ∧ ◡ 𝐹 = ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) ) )
38 37 simpld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 𝐴 [,] 𝐵 ) )
39 f1of ⊢ ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 𝐴 [,] 𝐵 ) → 𝐹 : ( 0 [,] 1 ) ⟶ ( 𝐴 [,] 𝐵 ) )
40 frn ⊢ ( 𝐹 : ( 0 [,] 1 ) ⟶ ( 𝐴 [,] 𝐵 ) → ran 𝐹 ⊆ ( 𝐴 [,] 𝐵 ) )
41 38 39 40 3syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ran 𝐹 ⊆ ( 𝐴 [,] 𝐵 ) )
42 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
43 42 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
44 ax-resscn ⊢ ℝ ⊆ ℂ
45 43 44 sstrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
46 cnrest2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ran 𝐹 ⊆ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℂ ) → ( 𝐹 ∈ ( II Cn 𝐽 ) ↔ 𝐹 ∈ ( II Cn ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ) ) )
47 14 41 45 46 mp3an2i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐹 ∈ ( II Cn 𝐽 ) ↔ 𝐹 ∈ ( II Cn ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ) ) )
48 36 47 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐹 ∈ ( II Cn ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ) )
49 37 simprd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ◡ 𝐹 = ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) )
50 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℂ ) → ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 [,] 𝐵 ) ) )
51 14 45 50 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 [,] 𝐵 ) ) )
52 cnrest2r ⊢ ( 𝐽 ∈ Top → ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ) ⊆ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) )
53 8 52 ax-mp ⊢ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ) ⊆ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 )
54 51 cnmptid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑦 ) ∈ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ) )
55 53 54 sselid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑦 ) ∈ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) )
56 51 15 29 cnmptc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐴 ) ∈ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) )
57 51 55 56 26 cnmpt12f ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑦 − 𝐴 ) ) ∈ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) )
58 difrp ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( 𝐵 − 𝐴 ) ∈ ℝ+ ) )
59 58 biimp3a ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐵 − 𝐴 ) ∈ ℝ+ )
60 rpcnne0 ⊢ ( ( 𝐵 − 𝐴 ) ∈ ℝ+ → ( ( 𝐵 − 𝐴 ) ∈ ℂ ∧ ( 𝐵 − 𝐴 ) ≠ 0 ) )
61 1 divccn ⊢ ( ( ( 𝐵 − 𝐴 ) ∈ ℂ ∧ ( 𝐵 − 𝐴 ) ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / ( 𝐵 − 𝐴 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
62 59 60 61 3syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / ( 𝐵 − 𝐴 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
63 oveq1 ⊢ ( 𝑥 = ( 𝑦 − 𝐴 ) → ( 𝑥 / ( 𝐵 − 𝐴 ) ) = ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) )
64 51 57 15 62 63 cnmpt11 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) ∈ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) )
65 49 64 eqeltrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ◡ 𝐹 ∈ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) )
66 dfdm4 ⊢ dom 𝐹 = ran ◡ 𝐹
67 66 eqimss2i ⊢ ran ◡ 𝐹 ⊆ dom 𝐹
68 f1odm ⊢ ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 𝐴 [,] 𝐵 ) → dom 𝐹 = ( 0 [,] 1 ) )
69 38 68 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → dom 𝐹 = ( 0 [,] 1 ) )
70 67 69 sseqtrid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ran ◡ 𝐹 ⊆ ( 0 [,] 1 ) )
71 unitsscn ⊢ ( 0 [,] 1 ) ⊆ ℂ
72 71 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 0 [,] 1 ) ⊆ ℂ )
73 cnrest2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ran ◡ 𝐹 ⊆ ( 0 [,] 1 ) ∧ ( 0 [,] 1 ) ⊆ ℂ ) → ( ◡ 𝐹 ∈ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) ↔ ◡ 𝐹 ∈ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( 𝐽 ↾t ( 0 [,] 1 ) ) ) ) )
74 14 70 72 73 mp3an2i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ◡ 𝐹 ∈ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) ↔ ◡ 𝐹 ∈ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( 𝐽 ↾t ( 0 [,] 1 ) ) ) ) )
75 65 74 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ◡ 𝐹 ∈ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( 𝐽 ↾t ( 0 [,] 1 ) ) ) )
76 5 oveq2i ⊢ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn II ) = ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( 𝐽 ↾t ( 0 [,] 1 ) ) )
77 75 76 eleqtrrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ◡ 𝐹 ∈ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn II ) )
78 ishmeo ⊢ ( 𝐹 ∈ ( II Homeo ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ) ↔ ( 𝐹 ∈ ( II Cn ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ) ∧ ◡ 𝐹 ∈ ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) Cn II ) ) )
79 48 77 78 sylanbrc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐹 ∈ ( II Homeo ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ) )