# 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 ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
icchmeo.f ${⊢}{F}=\left({x}\in \left[0,1\right]⟼{x}{B}+\left(1-{x}\right){A}\right)$
Assertion icchmeo ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {F}\in \left(\mathrm{II}\mathrm{Homeo}\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\right)$

### Proof

Step Hyp Ref Expression
1 icchmeo.j ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 icchmeo.f ${⊢}{F}=\left({x}\in \left[0,1\right]⟼{x}{B}+\left(1-{x}\right){A}\right)$
3 iitopon ${⊢}\mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
4 3 a1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
5 1 dfii3 ${⊢}\mathrm{II}={J}{↾}_{𝑡}\left[0,1\right]$
6 5 oveq2i ${⊢}\mathrm{II}\mathrm{Cn}\mathrm{II}=\mathrm{II}\mathrm{Cn}\left({J}{↾}_{𝑡}\left[0,1\right]\right)$
7 1 cnfldtop ${⊢}{J}\in \mathrm{Top}$
8 cnrest2r ${⊢}{J}\in \mathrm{Top}\to \mathrm{II}\mathrm{Cn}\left({J}{↾}_{𝑡}\left[0,1\right]\right)\subseteq \mathrm{II}\mathrm{Cn}{J}$
9 7 8 ax-mp ${⊢}\mathrm{II}\mathrm{Cn}\left({J}{↾}_{𝑡}\left[0,1\right]\right)\subseteq \mathrm{II}\mathrm{Cn}{J}$
10 6 9 eqsstri ${⊢}\mathrm{II}\mathrm{Cn}\mathrm{II}\subseteq \mathrm{II}\mathrm{Cn}{J}$
11 4 cnmptid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({x}\in \left[0,1\right]⟼{x}\right)\in \left(\mathrm{II}\mathrm{Cn}\mathrm{II}\right)$
12 10 11 sseldi ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({x}\in \left[0,1\right]⟼{x}\right)\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
13 1 cnfldtopon ${⊢}{J}\in \mathrm{TopOn}\left(ℂ\right)$
14 13 a1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {J}\in \mathrm{TopOn}\left(ℂ\right)$
15 simp2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {B}\in ℝ$
16 15 recnd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {B}\in ℂ$
17 4 14 16 cnmptc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({x}\in \left[0,1\right]⟼{B}\right)\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
18 1 mulcn ${⊢}×\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$
19 18 a1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to ×\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$
20 4 12 17 19 cnmpt12f ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({x}\in \left[0,1\right]⟼{x}{B}\right)\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
21 1cnd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to 1\in ℂ$
22 4 14 21 cnmptc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({x}\in \left[0,1\right]⟼1\right)\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
23 1 subcn ${⊢}-\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$
24 23 a1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to -\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$
25 4 22 12 24 cnmpt12f ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({x}\in \left[0,1\right]⟼1-{x}\right)\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
26 simp1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {A}\in ℝ$
27 26 recnd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {A}\in ℂ$
28 4 14 27 cnmptc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({x}\in \left[0,1\right]⟼{A}\right)\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
29 4 25 28 19 cnmpt12f ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({x}\in \left[0,1\right]⟼\left(1-{x}\right){A}\right)\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
30 1 addcn ${⊢}+\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$
31 30 a1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to +\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$
32 4 20 29 31 cnmpt12f ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({x}\in \left[0,1\right]⟼{x}{B}+\left(1-{x}\right){A}\right)\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
33 2 32 eqeltrid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
34 2 iccf1o ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({F}:\left[0,1\right]\underset{1-1 onto}{⟶}\left[{A},{B}\right]\wedge {{F}}^{-1}=\left({y}\in \left[{A},{B}\right]⟼\frac{{y}-{A}}{{B}-{A}}\right)\right)$
35 34 simpld ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {F}:\left[0,1\right]\underset{1-1 onto}{⟶}\left[{A},{B}\right]$
36 f1of ${⊢}{F}:\left[0,1\right]\underset{1-1 onto}{⟶}\left[{A},{B}\right]\to {F}:\left[0,1\right]⟶\left[{A},{B}\right]$
37 frn ${⊢}{F}:\left[0,1\right]⟶\left[{A},{B}\right]\to \mathrm{ran}{F}\subseteq \left[{A},{B}\right]$
38 35 36 37 3syl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \mathrm{ran}{F}\subseteq \left[{A},{B}\right]$
39 iccssre ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\subseteq ℝ$
40 39 3adant3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left[{A},{B}\right]\subseteq ℝ$
41 ax-resscn ${⊢}ℝ\subseteq ℂ$
42 40 41 sstrdi ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left[{A},{B}\right]\subseteq ℂ$
43 cnrest2 ${⊢}\left({J}\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{ran}{F}\subseteq \left[{A},{B}\right]\wedge \left[{A},{B}\right]\subseteq ℂ\right)\to \left({F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)↔{F}\in \left(\mathrm{II}\mathrm{Cn}\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\right)\right)$
44 13 38 42 43 mp3an2i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)↔{F}\in \left(\mathrm{II}\mathrm{Cn}\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\right)\right)$
45 33 44 mpbid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {F}\in \left(\mathrm{II}\mathrm{Cn}\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\right)$
46 34 simprd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {{F}}^{-1}=\left({y}\in \left[{A},{B}\right]⟼\frac{{y}-{A}}{{B}-{A}}\right)$
47 resttopon ${⊢}\left({J}\in \mathrm{TopOn}\left(ℂ\right)\wedge \left[{A},{B}\right]\subseteq ℂ\right)\to {J}{↾}_{𝑡}\left[{A},{B}\right]\in \mathrm{TopOn}\left(\left[{A},{B}\right]\right)$
48 13 42 47 sylancr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {J}{↾}_{𝑡}\left[{A},{B}\right]\in \mathrm{TopOn}\left(\left[{A},{B}\right]\right)$
49 cnrest2r ${⊢}{J}\in \mathrm{Top}\to \left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\subseteq \left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}{J}$
50 7 49 ax-mp ${⊢}\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\subseteq \left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}{J}$
51 48 cnmptid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({y}\in \left[{A},{B}\right]⟼{y}\right)\in \left(\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\right)$
52 50 51 sseldi ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({y}\in \left[{A},{B}\right]⟼{y}\right)\in \left(\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}{J}\right)$
53 48 14 27 cnmptc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({y}\in \left[{A},{B}\right]⟼{A}\right)\in \left(\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}{J}\right)$
54 48 52 53 24 cnmpt12f ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({y}\in \left[{A},{B}\right]⟼{y}-{A}\right)\in \left(\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}{J}\right)$
55 difrp ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}<{B}↔{B}-{A}\in {ℝ}^{+}\right)$
56 55 biimp3a ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {B}-{A}\in {ℝ}^{+}$
57 56 rpcnd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {B}-{A}\in ℂ$
58 56 rpne0d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {B}-{A}\ne 0$
59 1 divccn ${⊢}\left({B}-{A}\in ℂ\wedge {B}-{A}\ne 0\right)\to \left({x}\in ℂ⟼\frac{{x}}{{B}-{A}}\right)\in \left({J}\mathrm{Cn}{J}\right)$
60 57 58 59 syl2anc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({x}\in ℂ⟼\frac{{x}}{{B}-{A}}\right)\in \left({J}\mathrm{Cn}{J}\right)$
61 oveq1 ${⊢}{x}={y}-{A}\to \frac{{x}}{{B}-{A}}=\frac{{y}-{A}}{{B}-{A}}$
62 48 54 14 60 61 cnmpt11 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({y}\in \left[{A},{B}\right]⟼\frac{{y}-{A}}{{B}-{A}}\right)\in \left(\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}{J}\right)$
63 46 62 eqeltrd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {{F}}^{-1}\in \left(\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}{J}\right)$
64 dfdm4 ${⊢}\mathrm{dom}{F}=\mathrm{ran}{{F}}^{-1}$
65 64 eqimss2i ${⊢}\mathrm{ran}{{F}}^{-1}\subseteq \mathrm{dom}{F}$
66 f1odm ${⊢}{F}:\left[0,1\right]\underset{1-1 onto}{⟶}\left[{A},{B}\right]\to \mathrm{dom}{F}=\left[0,1\right]$
67 35 66 syl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \mathrm{dom}{F}=\left[0,1\right]$
68 65 67 sseqtrid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \mathrm{ran}{{F}}^{-1}\subseteq \left[0,1\right]$
69 unitssre ${⊢}\left[0,1\right]\subseteq ℝ$
70 69 a1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left[0,1\right]\subseteq ℝ$
71 70 41 sstrdi ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left[0,1\right]\subseteq ℂ$
72 cnrest2 ${⊢}\left({J}\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{ran}{{F}}^{-1}\subseteq \left[0,1\right]\wedge \left[0,1\right]\subseteq ℂ\right)\to \left({{F}}^{-1}\in \left(\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}{J}\right)↔{{F}}^{-1}\in \left(\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}\left({J}{↾}_{𝑡}\left[0,1\right]\right)\right)\right)$
73 13 68 71 72 mp3an2i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({{F}}^{-1}\in \left(\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}{J}\right)↔{{F}}^{-1}\in \left(\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}\left({J}{↾}_{𝑡}\left[0,1\right]\right)\right)\right)$
74 63 73 mpbid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {{F}}^{-1}\in \left(\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}\left({J}{↾}_{𝑡}\left[0,1\right]\right)\right)$
75 5 oveq2i ${⊢}\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}\mathrm{II}=\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}\left({J}{↾}_{𝑡}\left[0,1\right]\right)$
76 74 75 eleqtrrdi ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {{F}}^{-1}\in \left(\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}\mathrm{II}\right)$
77 ishmeo ${⊢}{F}\in \left(\mathrm{II}\mathrm{Homeo}\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\right)↔\left({F}\in \left(\mathrm{II}\mathrm{Cn}\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\right)\wedge {{F}}^{-1}\in \left(\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\mathrm{Cn}\mathrm{II}\right)\right)$
78 45 76 77 sylanbrc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {F}\in \left(\mathrm{II}\mathrm{Homeo}\left({J}{↾}_{𝑡}\left[{A},{B}\right]\right)\right)$