# Metamath Proof Explorer

## Theorem cnrehmeo

Description: The canonical bijection from ( RR X. RR ) to CC described in cnref1o is in fact a homeomorphism of the usual topologies on these sets. (It is also an isometry, if ( RR X. RR ) is metrized with the l2 norm.) (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses cnrehmeo.1 ${⊢}{F}=\left({x}\in ℝ,{y}\in ℝ⟼{x}+\mathrm{i}{y}\right)$
cnrehmeo.2 ${⊢}{J}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
cnrehmeo.3 ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
Assertion cnrehmeo ${⊢}{F}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Homeo}{K}\right)$

### Proof

Step Hyp Ref Expression
1 cnrehmeo.1 ${⊢}{F}=\left({x}\in ℝ,{y}\in ℝ⟼{x}+\mathrm{i}{y}\right)$
2 cnrehmeo.2 ${⊢}{J}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
3 cnrehmeo.3 ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
4 retopon ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$
5 2 4 eqeltri ${⊢}{J}\in \mathrm{TopOn}\left(ℝ\right)$
6 5 a1i ${⊢}\top \to {J}\in \mathrm{TopOn}\left(ℝ\right)$
7 3 cnfldtop ${⊢}{K}\in \mathrm{Top}$
8 cnrest2r ${⊢}{K}\in \mathrm{Top}\to \left({J}{×}_{t}{J}\right)\mathrm{Cn}\left({K}{↾}_{𝑡}ℝ\right)\subseteq \left({J}{×}_{t}{J}\right)\mathrm{Cn}{K}$
9 7 8 mp1i ${⊢}\top \to \left({J}{×}_{t}{J}\right)\mathrm{Cn}\left({K}{↾}_{𝑡}ℝ\right)\subseteq \left({J}{×}_{t}{J}\right)\mathrm{Cn}{K}$
10 6 6 cnmpt1st ${⊢}\top \to \left({x}\in ℝ,{y}\in ℝ⟼{x}\right)\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$
11 3 tgioo2 ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)={K}{↾}_{𝑡}ℝ$
12 2 11 eqtri ${⊢}{J}={K}{↾}_{𝑡}ℝ$
13 12 oveq2i ${⊢}\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}=\left({J}{×}_{t}{J}\right)\mathrm{Cn}\left({K}{↾}_{𝑡}ℝ\right)$
14 10 13 eleqtrdi ${⊢}\top \to \left({x}\in ℝ,{y}\in ℝ⟼{x}\right)\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}\left({K}{↾}_{𝑡}ℝ\right)\right)$
15 9 14 sseldd ${⊢}\top \to \left({x}\in ℝ,{y}\in ℝ⟼{x}\right)\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)$
16 3 cnfldtopon ${⊢}{K}\in \mathrm{TopOn}\left(ℂ\right)$
17 16 a1i ${⊢}\top \to {K}\in \mathrm{TopOn}\left(ℂ\right)$
18 ax-icn ${⊢}\mathrm{i}\in ℂ$
19 18 a1i ${⊢}\top \to \mathrm{i}\in ℂ$
20 6 6 17 19 cnmpt2c ${⊢}\top \to \left({x}\in ℝ,{y}\in ℝ⟼\mathrm{i}\right)\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)$
21 6 6 cnmpt2nd ${⊢}\top \to \left({x}\in ℝ,{y}\in ℝ⟼{y}\right)\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$
22 21 13 eleqtrdi ${⊢}\top \to \left({x}\in ℝ,{y}\in ℝ⟼{y}\right)\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}\left({K}{↾}_{𝑡}ℝ\right)\right)$
23 9 22 sseldd ${⊢}\top \to \left({x}\in ℝ,{y}\in ℝ⟼{y}\right)\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)$
24 3 mulcn ${⊢}×\in \left(\left({K}{×}_{t}{K}\right)\mathrm{Cn}{K}\right)$
25 24 a1i ${⊢}\top \to ×\in \left(\left({K}{×}_{t}{K}\right)\mathrm{Cn}{K}\right)$
26 6 6 20 23 25 cnmpt22f ${⊢}\top \to \left({x}\in ℝ,{y}\in ℝ⟼\mathrm{i}{y}\right)\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)$
27 3 addcn ${⊢}+\in \left(\left({K}{×}_{t}{K}\right)\mathrm{Cn}{K}\right)$
28 27 a1i ${⊢}\top \to +\in \left(\left({K}{×}_{t}{K}\right)\mathrm{Cn}{K}\right)$
29 6 6 15 26 28 cnmpt22f ${⊢}\top \to \left({x}\in ℝ,{y}\in ℝ⟼{x}+\mathrm{i}{y}\right)\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)$
30 1 29 eqeltrid ${⊢}\top \to {F}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)$
31 1 cnrecnv ${⊢}{{F}}^{-1}=\left({z}\in ℂ⟼⟨\Re \left({z}\right),\Im \left({z}\right)⟩\right)$
32 ref ${⊢}\Re :ℂ⟶ℝ$
33 32 a1i ${⊢}\top \to \Re :ℂ⟶ℝ$
34 33 feqmptd ${⊢}\top \to \Re =\left({z}\in ℂ⟼\Re \left({z}\right)\right)$
35 recncf ${⊢}\Re :ℂ\underset{cn}{⟶}ℝ$
36 ssid ${⊢}ℂ\subseteq ℂ$
37 ax-resscn ${⊢}ℝ\subseteq ℂ$
38 16 toponrestid ${⊢}{K}={K}{↾}_{𝑡}ℂ$
39 3 38 12 cncfcn
40 36 37 39 mp2an
41 35 40 eleqtri ${⊢}\Re \in \left({K}\mathrm{Cn}{J}\right)$
42 34 41 eqeltrrdi ${⊢}\top \to \left({z}\in ℂ⟼\Re \left({z}\right)\right)\in \left({K}\mathrm{Cn}{J}\right)$
43 imf ${⊢}\Im :ℂ⟶ℝ$
44 43 a1i ${⊢}\top \to \Im :ℂ⟶ℝ$
45 44 feqmptd ${⊢}\top \to \Im =\left({z}\in ℂ⟼\Im \left({z}\right)\right)$
46 imcncf ${⊢}\Im :ℂ\underset{cn}{⟶}ℝ$
47 46 40 eleqtri ${⊢}\Im \in \left({K}\mathrm{Cn}{J}\right)$
48 45 47 eqeltrrdi ${⊢}\top \to \left({z}\in ℂ⟼\Im \left({z}\right)\right)\in \left({K}\mathrm{Cn}{J}\right)$
49 17 42 48 cnmpt1t ${⊢}\top \to \left({z}\in ℂ⟼⟨\Re \left({z}\right),\Im \left({z}\right)⟩\right)\in \left({K}\mathrm{Cn}\left({J}{×}_{t}{J}\right)\right)$
50 31 49 eqeltrid ${⊢}\top \to {{F}}^{-1}\in \left({K}\mathrm{Cn}\left({J}{×}_{t}{J}\right)\right)$
51 ishmeo ${⊢}{F}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Homeo}{K}\right)↔\left({F}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)\wedge {{F}}^{-1}\in \left({K}\mathrm{Cn}\left({J}{×}_{t}{J}\right)\right)\right)$
52 30 50 51 sylanbrc ${⊢}\top \to {F}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Homeo}{K}\right)$
53 52 mptru ${⊢}{F}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Homeo}{K}\right)$