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)

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