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 l² norm.) (Contributed by Mario Carneiro, 25-Aug-2014)

	Ref	Expression
Hypotheses	cnrehmeo.1	⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
	cnrehmeo.2	⊢ 𝐽 = ( topGen ‘ ran (,) )
	cnrehmeo.3	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
Assertion	cnrehmeo	⊢ 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Homeo 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		cnrehmeo.1	⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
2		cnrehmeo.2	⊢ 𝐽 = ( topGen ‘ ran (,) )
3		cnrehmeo.3	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
4		retopon	⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
5	2 4	eqeltri	⊢ 𝐽 ∈ ( TopOn ‘ ℝ )
6	5	a1i	⊢ ( ⊤ → 𝐽 ∈ ( TopOn ‘ ℝ ) )
7	3	cnfldtop	⊢ 𝐾 ∈ Top
8		cnrest2r	⊢ ( 𝐾 ∈ Top → ( ( 𝐽 ×t 𝐽 ) Cn ( 𝐾 ↾t ℝ ) ) ⊆ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
9	7 8	mp1i	⊢ ( ⊤ → ( ( 𝐽 ×t 𝐽 ) Cn ( 𝐾 ↾t ℝ ) ) ⊆ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
10	6 6	cnmpt1st	⊢ ( ⊤ → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ 𝑥 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
11	3	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( 𝐾 ↾t ℝ )
12	2 11	eqtri	⊢ 𝐽 = ( 𝐾 ↾t ℝ )
13	12	oveq2i	⊢ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) = ( ( 𝐽 ×t 𝐽 ) Cn ( 𝐾 ↾t ℝ ) )
14	10 13	eleqtrdi	⊢ ( ⊤ → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ 𝑥 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( 𝐾 ↾t ℝ ) ) )
15	9 14	sseldd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ 𝑥 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
16	3	cnfldtopon	⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
17	16	a1i	⊢ ( ⊤ → 𝐾 ∈ ( TopOn ‘ ℂ ) )
18		ax-icn	⊢ i ∈ ℂ
19	18	a1i	⊢ ( ⊤ → i ∈ ℂ )
20	6 6 17 19	cnmpt2c	⊢ ( ⊤ → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ i ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
21	6 6	cnmpt2nd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ 𝑦 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
22	21 13	eleqtrdi	⊢ ( ⊤ → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ 𝑦 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( 𝐾 ↾t ℝ ) ) )
23	9 22	sseldd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ 𝑦 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
24	3	mulcn	⊢ · ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
25	24	a1i	⊢ ( ⊤ → · ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
26	6 6 20 23 25	cnmpt22f	⊢ ( ⊤ → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( i · 𝑦 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
27	3	addcn	⊢ + ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
28	27	a1i	⊢ ( ⊤ → + ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
29	6 6 15 26 28	cnmpt22f	⊢ ( ⊤ → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
30	1 29	eqeltrid	⊢ ( ⊤ → 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
31	1	cnrecnv	⊢ ◡ 𝐹 = ( 𝑧 ∈ ℂ ↦ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ )
32		ref	⊢ ℜ : ℂ ⟶ ℝ
33	32	a1i	⊢ ( ⊤ → ℜ : ℂ ⟶ ℝ )
34	33	feqmptd	⊢ ( ⊤ → ℜ = ( 𝑧 ∈ ℂ ↦ ( ℜ ‘ 𝑧 ) ) )
35		recncf	⊢ ℜ ∈ ( ℂ –cn→ ℝ )
36		ssid	⊢ ℂ ⊆ ℂ
37		ax-resscn	⊢ ℝ ⊆ ℂ
38	16	toponrestid	⊢ 𝐾 = ( 𝐾 ↾t ℂ )
39	3 38 12	cncfcn	⊢ ( ( ℂ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℂ –cn→ ℝ ) = ( 𝐾 Cn 𝐽 ) )
40	36 37 39	mp2an	⊢ ( ℂ –cn→ ℝ ) = ( 𝐾 Cn 𝐽 )
41	35 40	eleqtri	⊢ ℜ ∈ ( 𝐾 Cn 𝐽 )
42	34 41	eqeltrrdi	⊢ ( ⊤ → ( 𝑧 ∈ ℂ ↦ ( ℜ ‘ 𝑧 ) ) ∈ ( 𝐾 Cn 𝐽 ) )
43		imf	⊢ ℑ : ℂ ⟶ ℝ
44	43	a1i	⊢ ( ⊤ → ℑ : ℂ ⟶ ℝ )
45	44	feqmptd	⊢ ( ⊤ → ℑ = ( 𝑧 ∈ ℂ ↦ ( ℑ ‘ 𝑧 ) ) )
46		imcncf	⊢ ℑ ∈ ( ℂ –cn→ ℝ )
47	46 40	eleqtri	⊢ ℑ ∈ ( 𝐾 Cn 𝐽 )
48	45 47	eqeltrrdi	⊢ ( ⊤ → ( 𝑧 ∈ ℂ ↦ ( ℑ ‘ 𝑧 ) ) ∈ ( 𝐾 Cn 𝐽 ) )
49	17 42 48	cnmpt1t	⊢ ( ⊤ → ( 𝑧 ∈ ℂ ↦ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ ) ∈ ( 𝐾 Cn ( 𝐽 ×t 𝐽 ) ) )
50	31 49	eqeltrid	⊢ ( ⊤ → ◡ 𝐹 ∈ ( 𝐾 Cn ( 𝐽 ×t 𝐽 ) ) )
51		ishmeo	⊢ ( 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Homeo 𝐾 ) ↔ ( 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) ∧ ◡ 𝐹 ∈ ( 𝐾 Cn ( 𝐽 ×t 𝐽 ) ) ) )
52	30 50 51	sylanbrc	⊢ ( ⊤ → 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Homeo 𝐾 ) )
53	52	mptru	⊢ 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Homeo 𝐾 )