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 syl5eqr ⊢ ( 𝑧 ∈ ℂ → ( 𝐹 ‘ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ ) = ( ( ℜ ‘ 𝑧 ) + ( 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 ⊢ ◡ 𝐹 = ( 𝑧 ∈ ℂ ↦ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ )