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) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

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 mpomulcn ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
25 24 a1i ⊢ ( ⊤ → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
26 oveq12 ⊢ ( ( 𝑢 = i ∧ 𝑣 = 𝑦 ) → ( 𝑢 · 𝑣 ) = ( i · 𝑦 ) )
27 6 6 20 23 17 17 25 26 cnmpt22 ⊢ ( ⊤ → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( i · 𝑦 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
28 3 addcn ⊢ + ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
29 28 a1i ⊢ ( ⊤ → + ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
30 6 6 15 27 29 cnmpt22f ⊢ ( ⊤ → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
31 1 30 eqeltrid ⊢ ( ⊤ → 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
32 1 cnrecnv ⊢ ◡ 𝐹 = ( 𝑧 ∈ ℂ ↦ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ )
33 ref ⊢ ℜ : ℂ ⟶ ℝ
34 33 a1i ⊢ ( ⊤ → ℜ : ℂ ⟶ ℝ )
35 34 feqmptd ⊢ ( ⊤ → ℜ = ( 𝑧 ∈ ℂ ↦ ( ℜ ‘ 𝑧 ) ) )
36 recncf ⊢ ℜ ∈ ( ℂ –cn→ ℝ )
37 ssid ⊢ ℂ ⊆ ℂ
38 ax-resscn ⊢ ℝ ⊆ ℂ
39 16 toponrestid ⊢ 𝐾 = ( 𝐾 ↾t ℂ )
40 3 39 12 cncfcn ⊢ ( ( ℂ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℂ –cn→ ℝ ) = ( 𝐾 Cn 𝐽 ) )
41 37 38 40 mp2an ⊢ ( ℂ –cn→ ℝ ) = ( 𝐾 Cn 𝐽 )
42 36 41 eleqtri ⊢ ℜ ∈ ( 𝐾 Cn 𝐽 )
43 35 42 eqeltrrdi ⊢ ( ⊤ → ( 𝑧 ∈ ℂ ↦ ( ℜ ‘ 𝑧 ) ) ∈ ( 𝐾 Cn 𝐽 ) )
44 imf ⊢ ℑ : ℂ ⟶ ℝ
45 44 a1i ⊢ ( ⊤ → ℑ : ℂ ⟶ ℝ )
46 45 feqmptd ⊢ ( ⊤ → ℑ = ( 𝑧 ∈ ℂ ↦ ( ℑ ‘ 𝑧 ) ) )
47 imcncf ⊢ ℑ ∈ ( ℂ –cn→ ℝ )
48 47 41 eleqtri ⊢ ℑ ∈ ( 𝐾 Cn 𝐽 )
49 46 48 eqeltrrdi ⊢ ( ⊤ → ( 𝑧 ∈ ℂ ↦ ( ℑ ‘ 𝑧 ) ) ∈ ( 𝐾 Cn 𝐽 ) )
50 17 43 49 cnmpt1t ⊢ ( ⊤ → ( 𝑧 ∈ ℂ ↦ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ ) ∈ ( 𝐾 Cn ( 𝐽 ×t 𝐽 ) ) )
51 32 50 eqeltrid ⊢ ( ⊤ → ◡ 𝐹 ∈ ( 𝐾 Cn ( 𝐽 ×t 𝐽 ) ) )
52 ishmeo ⊢ ( 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Homeo 𝐾 ) ↔ ( 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) ∧ ◡ 𝐹 ∈ ( 𝐾 Cn ( 𝐽 ×t 𝐽 ) ) ) )
53 31 51 52 sylanbrc ⊢ ( ⊤ → 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Homeo 𝐾 ) )
54 53 mptru ⊢ 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Homeo 𝐾 )