This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnrehmeoOLD

Description: Obsolete version of cnrehmeo as of 9-Apr-2025. (Contributed by Mario Carneiro, 25-Aug-2014) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cnrehmeoOLD.1 ⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
2 cnrehmeoOLD.2 ⊢ 𝐽 = ( topGen ‘ ran (,) )
3 cnrehmeoOLD.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 𝐾 )