Metamath Proof Explorer


Theorem cnref1o

Description: There is a natural one-to-one mapping from ( RR X. RR ) to CC , where we map <. x , y >. to ( x + (i x. y ) ) . In our construction of the complex numbers, this is in fact our definition_ of CC (see df-c ), but in the axiomatic treatment we can only show that there is the expected mapping between these two sets. (Contributed by Mario Carneiro, 16-Jun-2013) (Revised by Mario Carneiro, 17-Feb-2014)

Ref Expression
Hypothesis cnref1o.1 F = x , y x + i y
Assertion cnref1o F : 2 1-1 onto

Proof

Step Hyp Ref Expression
1 cnref1o.1 F = x , y x + i y
2 ovex x + i y V
3 1 2 fnmpoi F Fn 2
4 1st2nd2 z 2 z = 1 st z 2 nd z
5 4 fveq2d z 2 F z = F 1 st z 2 nd z
6 df-ov 1 st z F 2 nd z = F 1 st z 2 nd z
7 5 6 eqtr4di z 2 F z = 1 st z F 2 nd z
8 xp1st z 2 1 st z
9 xp2nd z 2 2 nd z
10 oveq1 x = 1 st z x + i y = 1 st z + i y
11 oveq2 y = 2 nd z i y = i 2 nd z
12 11 oveq2d y = 2 nd z 1 st z + i y = 1 st z + i 2 nd z
13 ovex 1 st z + i 2 nd z V
14 10 12 1 13 ovmpo 1 st z 2 nd z 1 st z F 2 nd z = 1 st z + i 2 nd z
15 8 9 14 syl2anc z 2 1 st z F 2 nd z = 1 st z + i 2 nd z
16 7 15 eqtrd z 2 F z = 1 st z + i 2 nd z
17 8 recnd z 2 1 st z
18 ax-icn i
19 9 recnd z 2 2 nd z
20 mulcl i 2 nd z i 2 nd z
21 18 19 20 sylancr z 2 i 2 nd z
22 17 21 addcld z 2 1 st z + i 2 nd z
23 16 22 eqeltrd z 2 F z
24 23 rgen z 2 F z
25 ffnfv F : 2 F Fn 2 z 2 F z
26 3 24 25 mpbir2an F : 2
27 8 9 jca z 2 1 st z 2 nd z
28 xp1st w 2 1 st w
29 xp2nd w 2 2 nd w
30 28 29 jca w 2 1 st w 2 nd w
31 cru 1 st z 2 nd z 1 st w 2 nd w 1 st z + i 2 nd z = 1 st w + i 2 nd w 1 st z = 1 st w 2 nd z = 2 nd w
32 27 30 31 syl2an z 2 w 2 1 st z + i 2 nd z = 1 st w + i 2 nd w 1 st z = 1 st w 2 nd z = 2 nd w
33 fveq2 z = w F z = F w
34 fveq2 z = w 1 st z = 1 st w
35 fveq2 z = w 2 nd z = 2 nd w
36 35 oveq2d z = w i 2 nd z = i 2 nd w
37 34 36 oveq12d z = w 1 st z + i 2 nd z = 1 st w + i 2 nd w
38 33 37 eqeq12d z = w F z = 1 st z + i 2 nd z F w = 1 st w + i 2 nd w
39 38 16 vtoclga w 2 F w = 1 st w + i 2 nd w
40 16 39 eqeqan12d z 2 w 2 F z = F w 1 st z + i 2 nd z = 1 st w + i 2 nd w
41 1st2nd2 w 2 w = 1 st w 2 nd w
42 4 41 eqeqan12d z 2 w 2 z = w 1 st z 2 nd z = 1 st w 2 nd w
43 fvex 1 st z V
44 fvex 2 nd z V
45 43 44 opth 1 st z 2 nd z = 1 st w 2 nd w 1 st z = 1 st w 2 nd z = 2 nd w
46 42 45 bitrdi z 2 w 2 z = w 1 st z = 1 st w 2 nd z = 2 nd w
47 32 40 46 3bitr4d z 2 w 2 F z = F w z = w
48 47 biimpd z 2 w 2 F z = F w z = w
49 48 rgen2 z 2 w 2 F z = F w z = w
50 dff13 F : 2 1-1 F : 2 z 2 w 2 F z = F w z = w
51 26 49 50 mpbir2an F : 2 1-1
52 cnre w u v w = u + i v
53 oveq1 x = u x + i y = u + i y
54 oveq2 y = v i y = i v
55 54 oveq2d y = v u + i y = u + i v
56 ovex u + i v V
57 53 55 1 56 ovmpo u v u F v = u + i v
58 57 eqeq2d u v w = u F v w = u + i v
59 58 2rexbiia u v w = u F v u v w = u + i v
60 52 59 sylibr w u v w = u F v
61 fveq2 z = u v F z = F u v
62 df-ov u F v = F u v
63 61 62 eqtr4di z = u v F z = u F v
64 63 eqeq2d z = u v w = F z w = u F v
65 64 rexxp z 2 w = F z u v w = u F v
66 60 65 sylibr w z 2 w = F z
67 66 rgen w z 2 w = F z
68 dffo3 F : 2 onto F : 2 w z 2 w = F z
69 26 67 68 mpbir2an F : 2 onto
70 df-f1o F : 2 1-1 onto F : 2 1-1 F : 2 onto
71 51 69 70 mpbir2an F : 2 1-1 onto