Metamath Proof Explorer


Theorem cnrecnv

Description: The inverse to the canonical bijection from ( RR X. RR ) to CC from cnref1o . (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypothesis cnrecnv.1 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
Assertion cnrecnv 𝐹 = ( 𝑧 ∈ ℂ ↦ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ )

Proof

Step Hyp Ref Expression
1 cnrecnv.1 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
2 1 cnref1o 𝐹 : ( ℝ × ℝ ) –1-1-onto→ ℂ
3 f1ocnv ( 𝐹 : ( ℝ × ℝ ) –1-1-onto→ ℂ → 𝐹 : ℂ –1-1-onto→ ( ℝ × ℝ ) )
4 f1of ( 𝐹 : ℂ –1-1-onto→ ( ℝ × ℝ ) → 𝐹 : ℂ ⟶ ( ℝ × ℝ ) )
5 2 3 4 mp2b 𝐹 : ℂ ⟶ ( ℝ × ℝ )
6 5 a1i ( ⊤ → 𝐹 : ℂ ⟶ ( ℝ × ℝ ) )
7 6 feqmptd ( ⊤ → 𝐹 = ( 𝑧 ∈ ℂ ↦ ( 𝐹𝑧 ) ) )
8 7 mptru 𝐹 = ( 𝑧 ∈ ℂ ↦ ( 𝐹𝑧 ) )
9 df-ov ( ( ℜ ‘ 𝑧 ) 𝐹 ( ℑ ‘ 𝑧 ) ) = ( 𝐹 ‘ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ )
10 recl ( 𝑧 ∈ ℂ → ( ℜ ‘ 𝑧 ) ∈ ℝ )
11 imcl ( 𝑧 ∈ ℂ → ( ℑ ‘ 𝑧 ) ∈ ℝ )
12 oveq1 ( 𝑥 = ( ℜ ‘ 𝑧 ) → ( 𝑥 + ( i · 𝑦 ) ) = ( ( ℜ ‘ 𝑧 ) + ( i · 𝑦 ) ) )
13 oveq2 ( 𝑦 = ( ℑ ‘ 𝑧 ) → ( i · 𝑦 ) = ( i · ( ℑ ‘ 𝑧 ) ) )
14 13 oveq2d ( 𝑦 = ( ℑ ‘ 𝑧 ) → ( ( ℜ ‘ 𝑧 ) + ( i · 𝑦 ) ) = ( ( ℜ ‘ 𝑧 ) + ( i · ( ℑ ‘ 𝑧 ) ) ) )
15 ovex ( ( ℜ ‘ 𝑧 ) + ( i · ( ℑ ‘ 𝑧 ) ) ) ∈ V
16 12 14 1 15 ovmpo ( ( ( ℜ ‘ 𝑧 ) ∈ ℝ ∧ ( ℑ ‘ 𝑧 ) ∈ ℝ ) → ( ( ℜ ‘ 𝑧 ) 𝐹 ( ℑ ‘ 𝑧 ) ) = ( ( ℜ ‘ 𝑧 ) + ( i · ( ℑ ‘ 𝑧 ) ) ) )
17 10 11 16 syl2anc ( 𝑧 ∈ ℂ → ( ( ℜ ‘ 𝑧 ) 𝐹 ( ℑ ‘ 𝑧 ) ) = ( ( ℜ ‘ 𝑧 ) + ( i · ( ℑ ‘ 𝑧 ) ) ) )
18 9 17 eqtr3id ( 𝑧 ∈ ℂ → ( 𝐹 ‘ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ ) = ( ( ℜ ‘ 𝑧 ) + ( i · ( ℑ ‘ 𝑧 ) ) ) )
19 replim ( 𝑧 ∈ ℂ → 𝑧 = ( ( ℜ ‘ 𝑧 ) + ( i · ( ℑ ‘ 𝑧 ) ) ) )
20 18 19 eqtr4d ( 𝑧 ∈ ℂ → ( 𝐹 ‘ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ ) = 𝑧 )
21 20 fveq2d ( 𝑧 ∈ ℂ → ( 𝐹 ‘ ( 𝐹 ‘ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ ) ) = ( 𝐹𝑧 ) )
22 10 11 opelxpd ( 𝑧 ∈ ℂ → ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ ∈ ( ℝ × ℝ ) )
23 f1ocnvfv1 ( ( 𝐹 : ( ℝ × ℝ ) –1-1-onto→ ℂ ∧ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ ∈ ( ℝ × ℝ ) ) → ( 𝐹 ‘ ( 𝐹 ‘ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ ) ) = ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ )
24 2 22 23 sylancr ( 𝑧 ∈ ℂ → ( 𝐹 ‘ ( 𝐹 ‘ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ ) ) = ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ )
25 21 24 eqtr3d ( 𝑧 ∈ ℂ → ( 𝐹𝑧 ) = ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ )
26 25 mpteq2ia ( 𝑧 ∈ ℂ ↦ ( 𝐹𝑧 ) ) = ( 𝑧 ∈ ℂ ↦ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ )
27 8 26 eqtri 𝐹 = ( 𝑧 ∈ ℂ ↦ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ )