# 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}=\left({x}\in ℝ,{y}\in ℝ⟼{x}+\mathrm{i}{y}\right)$
Assertion cnref1o ${⊢}{F}:{ℝ}^{2}\underset{1-1 onto}{⟶}ℂ$

### Proof

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