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 F = x , y x + i y
Assertion cnrecnv F -1 = z z z

Proof

Step Hyp Ref Expression
1 cnrecnv.1 F = x , y x + i y
2 1 cnref1o F : 2 1-1 onto
3 f1ocnv F : 2 1-1 onto F -1 : 1-1 onto 2
4 f1of F -1 : 1-1 onto 2 F -1 : 2
5 2 3 4 mp2b F -1 : 2
6 5 a1i F -1 : 2
7 6 feqmptd F -1 = z F -1 z
8 7 mptru F -1 = z F -1 z
9 df-ov z F z = F z z
10 recl z z
11 imcl z z
12 oveq1 x = z x + i y = z + i y
13 oveq2 y = z i y = i z
14 13 oveq2d y = z z + i y = z + i z
15 ovex z + i z V
16 12 14 1 15 ovmpo z z z F z = z + i z
17 10 11 16 syl2anc z z F z = z + i z
18 9 17 eqtr3id z F z z = z + i z
19 replim z z = z + i z
20 18 19 eqtr4d z F z z = z
21 20 fveq2d z F -1 F z z = F -1 z
22 10 11 opelxpd z z z 2
23 f1ocnvfv1 F : 2 1-1 onto z z 2 F -1 F z z = z z
24 2 22 23 sylancr z F -1 F z z = z z
25 21 24 eqtr3d z F -1 z = z z
26 25 mpteq2ia z F -1 z = z z z
27 8 26 eqtri F -1 = z z z