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

Proof

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

Metamath Proof Explorer

Theorem cnref1o

Proof