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	$$⊢F=\left(x\in ℝ,y\in ℝ⟼x+\mathrm{i}y\right)$$
Assertion	cnrecnv	$$⊢F^{-1}=\left(z\in ℂ⟼⟨\Re \left(z\right),\Im \left(z\right)⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnrecnv.1	$$⊢F=\left(x\in ℝ,y\in ℝ⟼x+\mathrm{i}y\right)$$
2	1	cnref1o	$$⊢F:{ℝ}^2\underset{1-1\; onto}{⟶}ℂ$$
3		f1ocnv	$$⊢F:{ℝ}^2\underset{1-1\; onto}{⟶}ℂ\to F^{-1}:ℂ\underset{1-1\; onto}{⟶}{ℝ}^2$$
4		f1of	$$⊢F^{-1}:ℂ\underset{1-1\; onto}{⟶}{ℝ}^2\to F^{-1}:ℂ⟶{ℝ}^2$$
5	2 3 4	mp2b	$$⊢F^{-1}:ℂ⟶{ℝ}^2$$
6	5	a1i	$$⊢\top \to F^{-1}:ℂ⟶{ℝ}^2$$
7	6	feqmptd	$$⊢\top \to F^{-1}=\left(z\in ℂ⟼F^{-1}\left(z\right)\right)$$
8	7	mptru	$$⊢F^{-1}=\left(z\in ℂ⟼F^{-1}\left(z\right)\right)$$
9		df-ov	$$⊢\Re \left(z\right)F\Im \left(z\right)=F\left(⟨\Re \left(z\right),\Im \left(z\right)⟩\right)$$
10		recl	$$⊢z\in ℂ\to \Re \left(z\right)\in ℝ$$
11		imcl	$$⊢z\in ℂ\to \Im \left(z\right)\in ℝ$$
12		oveq1	$$⊢x=\Re \left(z\right)\to x+\mathrm{i}y=\Re \left(z\right)+\mathrm{i}y$$
13		oveq2	$$⊢y=\Im \left(z\right)\to \mathrm{i}y=\mathrm{i}\Im \left(z\right)$$
14	13	oveq2d	$$⊢y=\Im \left(z\right)\to \Re \left(z\right)+\mathrm{i}y=\Re \left(z\right)+\mathrm{i}\Im \left(z\right)$$
15		ovex	$$⊢\Re \left(z\right)+\mathrm{i}\Im \left(z\right)\in \mathrm{V}$$
16	12 14 1 15	ovmpo	$$⊢\left(\Re \left(z\right)\in ℝ\wedge \Im \left(z\right)\in ℝ\right)\to \Re \left(z\right)F\Im \left(z\right)=\Re \left(z\right)+\mathrm{i}\Im \left(z\right)$$
17	10 11 16	syl2anc	$$⊢z\in ℂ\to \Re \left(z\right)F\Im \left(z\right)=\Re \left(z\right)+\mathrm{i}\Im \left(z\right)$$
18	9 17	syl5eqr	$$⊢z\in ℂ\to F\left(⟨\Re \left(z\right),\Im \left(z\right)⟩\right)=\Re \left(z\right)+\mathrm{i}\Im \left(z\right)$$
19		replim	$$⊢z\in ℂ\to z=\Re \left(z\right)+\mathrm{i}\Im \left(z\right)$$
20	18 19	eqtr4d	$$⊢z\in ℂ\to F\left(⟨\Re \left(z\right),\Im \left(z\right)⟩\right)=z$$
21	20	fveq2d	$$⊢z\in ℂ\to F^{-1}\left(F\left(⟨\Re \left(z\right),\Im \left(z\right)⟩\right)\right)=F^{-1}\left(z\right)$$
22	10 11	opelxpd	$$⊢z\in ℂ\to ⟨\Re \left(z\right),\Im \left(z\right)⟩\in {ℝ}^2$$
23		f1ocnvfv1	$$⊢\left(F:{ℝ}^2\underset{1-1\; onto}{⟶}ℂ\wedge ⟨\Re \left(z\right),\Im \left(z\right)⟩\in {ℝ}^2\right)\to F^{-1}\left(F\left(⟨\Re \left(z\right),\Im \left(z\right)⟩\right)\right)=⟨\Re \left(z\right),\Im \left(z\right)⟩$$
24	2 22 23	sylancr	$$⊢z\in ℂ\to F^{-1}\left(F\left(⟨\Re \left(z\right),\Im \left(z\right)⟩\right)\right)=⟨\Re \left(z\right),\Im \left(z\right)⟩$$
25	21 24	eqtr3d	$$⊢z\in ℂ\to F^{-1}\left(z\right)=⟨\Re \left(z\right),\Im \left(z\right)⟩$$
26	25	mpteq2ia	$$⊢\left(z\in ℂ⟼F^{-1}\left(z\right)\right)=\left(z\in ℂ⟼⟨\Re \left(z\right),\Im \left(z\right)⟩\right)$$
27	8 26	eqtri	$$⊢F^{-1}=\left(z\in ℂ⟼⟨\Re \left(z\right),\Im \left(z\right)⟩\right)$$