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	⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
	Assertion	cnref1o	⊢ 𝐹 : ( ℝ × ℝ ) –1-1-onto→ ℂ

Proof

Step	Hyp	Ref	Expression
1		cnref1o.1	⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
2		ovex	⊢ ( 𝑥 + ( i · 𝑦 ) ) ∈ V
3	1 2	fnmpoi	⊢ 𝐹 Fn ( ℝ × ℝ )
4		1st2nd2	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
5	4	fveq2d	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) )
6		df-ov	⊢ ( ( 1^st ‘ 𝑧 ) 𝐹 ( 2^nd ‘ 𝑧 ) ) = ( 𝐹 ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
7	5 6	eqtr4di	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑧 ) = ( ( 1^st ‘ 𝑧 ) 𝐹 ( 2^nd ‘ 𝑧 ) ) )
8		xp1st	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 1^st ‘ 𝑧 ) ∈ ℝ )
9		xp2nd	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 2^nd ‘ 𝑧 ) ∈ ℝ )
10		oveq1	⊢ ( 𝑥 = ( 1^st ‘ 𝑧 ) → ( 𝑥 + ( i · 𝑦 ) ) = ( ( 1^st ‘ 𝑧 ) + ( i · 𝑦 ) ) )
11		oveq2	⊢ ( 𝑦 = ( 2^nd ‘ 𝑧 ) → ( i · 𝑦 ) = ( i · ( 2^nd ‘ 𝑧 ) ) )
12	11	oveq2d	⊢ ( 𝑦 = ( 2^nd ‘ 𝑧 ) → ( ( 1^st ‘ 𝑧 ) + ( i · 𝑦 ) ) = ( ( 1^st ‘ 𝑧 ) + ( i · ( 2^nd ‘ 𝑧 ) ) ) )
13		ovex	⊢ ( ( 1^st ‘ 𝑧 ) + ( i · ( 2^nd ‘ 𝑧 ) ) ) ∈ V
14	10 12 1 13	ovmpo	⊢ ( ( ( 1^st ‘ 𝑧 ) ∈ ℝ ∧ ( 2^nd ‘ 𝑧 ) ∈ ℝ ) → ( ( 1^st ‘ 𝑧 ) 𝐹 ( 2^nd ‘ 𝑧 ) ) = ( ( 1^st ‘ 𝑧 ) + ( i · ( 2^nd ‘ 𝑧 ) ) ) )
15	8 9 14	syl2anc	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( ( 1^st ‘ 𝑧 ) 𝐹 ( 2^nd ‘ 𝑧 ) ) = ( ( 1^st ‘ 𝑧 ) + ( i · ( 2^nd ‘ 𝑧 ) ) ) )
16	7 15	eqtrd	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑧 ) = ( ( 1^st ‘ 𝑧 ) + ( i · ( 2^nd ‘ 𝑧 ) ) ) )
17	8	recnd	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 1^st ‘ 𝑧 ) ∈ ℂ )
18		ax-icn	⊢ i ∈ ℂ
19	9	recnd	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 2^nd ‘ 𝑧 ) ∈ ℂ )
20		mulcl	⊢ ( ( i ∈ ℂ ∧ ( 2^nd ‘ 𝑧 ) ∈ ℂ ) → ( i · ( 2^nd ‘ 𝑧 ) ) ∈ ℂ )
21	18 19 20	sylancr	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( i · ( 2^nd ‘ 𝑧 ) ) ∈ ℂ )
22	17 21	addcld	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( ( 1^st ‘ 𝑧 ) + ( i · ( 2^nd ‘ 𝑧 ) ) ) ∈ ℂ )
23	16 22	eqeltrd	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
24	23	rgen	⊢ ∀ 𝑧 ∈ ( ℝ × ℝ ) ( 𝐹 ‘ 𝑧 ) ∈ ℂ
25		ffnfv	⊢ ( 𝐹 : ( ℝ × ℝ ) ⟶ ℂ ↔ ( 𝐹 Fn ( ℝ × ℝ ) ∧ ∀ 𝑧 ∈ ( ℝ × ℝ ) ( 𝐹 ‘ 𝑧 ) ∈ ℂ ) )
26	3 24 25	mpbir2an	⊢ 𝐹 : ( ℝ × ℝ ) ⟶ ℂ
27	8 9	jca	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( ( 1^st ‘ 𝑧 ) ∈ ℝ ∧ ( 2^nd ‘ 𝑧 ) ∈ ℝ ) )
28		xp1st	⊢ ( 𝑤 ∈ ( ℝ × ℝ ) → ( 1^st ‘ 𝑤 ) ∈ ℝ )
29		xp2nd	⊢ ( 𝑤 ∈ ( ℝ × ℝ ) → ( 2^nd ‘ 𝑤 ) ∈ ℝ )
30	28 29	jca	⊢ ( 𝑤 ∈ ( ℝ × ℝ ) → ( ( 1^st ‘ 𝑤 ) ∈ ℝ ∧ ( 2^nd ‘ 𝑤 ) ∈ ℝ ) )
31		cru	⊢ ( ( ( ( 1^st ‘ 𝑧 ) ∈ ℝ ∧ ( 2^nd ‘ 𝑧 ) ∈ ℝ ) ∧ ( ( 1^st ‘ 𝑤 ) ∈ ℝ ∧ ( 2^nd ‘ 𝑤 ) ∈ ℝ ) ) → ( ( ( 1^st ‘ 𝑧 ) + ( i · ( 2^nd ‘ 𝑧 ) ) ) = ( ( 1^st ‘ 𝑤 ) + ( i · ( 2^nd ‘ 𝑤 ) ) ) ↔ ( ( 1^st ‘ 𝑧 ) = ( 1^st ‘ 𝑤 ) ∧ ( 2^nd ‘ 𝑧 ) = ( 2^nd ‘ 𝑤 ) ) ) )
32	27 30 31	syl2an	⊢ ( ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ( ℝ × ℝ ) ) → ( ( ( 1^st ‘ 𝑧 ) + ( i · ( 2^nd ‘ 𝑧 ) ) ) = ( ( 1^st ‘ 𝑤 ) + ( i · ( 2^nd ‘ 𝑤 ) ) ) ↔ ( ( 1^st ‘ 𝑧 ) = ( 1^st ‘ 𝑤 ) ∧ ( 2^nd ‘ 𝑧 ) = ( 2^nd ‘ 𝑤 ) ) ) )
33		fveq2	⊢ ( 𝑧 = 𝑤 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) )
34		fveq2	⊢ ( 𝑧 = 𝑤 → ( 1^st ‘ 𝑧 ) = ( 1^st ‘ 𝑤 ) )
35		fveq2	⊢ ( 𝑧 = 𝑤 → ( 2^nd ‘ 𝑧 ) = ( 2^nd ‘ 𝑤 ) )
36	35	oveq2d	⊢ ( 𝑧 = 𝑤 → ( i · ( 2^nd ‘ 𝑧 ) ) = ( i · ( 2^nd ‘ 𝑤 ) ) )
37	34 36	oveq12d	⊢ ( 𝑧 = 𝑤 → ( ( 1^st ‘ 𝑧 ) + ( i · ( 2^nd ‘ 𝑧 ) ) ) = ( ( 1^st ‘ 𝑤 ) + ( i · ( 2^nd ‘ 𝑤 ) ) ) )
38	33 37	eqeq12d	⊢ ( 𝑧 = 𝑤 → ( ( 𝐹 ‘ 𝑧 ) = ( ( 1^st ‘ 𝑧 ) + ( i · ( 2^nd ‘ 𝑧 ) ) ) ↔ ( 𝐹 ‘ 𝑤 ) = ( ( 1^st ‘ 𝑤 ) + ( i · ( 2^nd ‘ 𝑤 ) ) ) ) )
39	38 16	vtoclga	⊢ ( 𝑤 ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑤 ) = ( ( 1^st ‘ 𝑤 ) + ( i · ( 2^nd ‘ 𝑤 ) ) ) )
40	16 39	eqeqan12d	⊢ ( ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ( ℝ × ℝ ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ( ( 1^st ‘ 𝑧 ) + ( i · ( 2^nd ‘ 𝑧 ) ) ) = ( ( 1^st ‘ 𝑤 ) + ( i · ( 2^nd ‘ 𝑤 ) ) ) ) )
41		1st2nd2	⊢ ( 𝑤 ∈ ( ℝ × ℝ ) → 𝑤 = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ )
42	4 41	eqeqan12d	⊢ ( ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ( ℝ × ℝ ) ) → ( 𝑧 = 𝑤 ↔ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) )
43		fvex	⊢ ( 1^st ‘ 𝑧 ) ∈ V
44		fvex	⊢ ( 2^nd ‘ 𝑧 ) ∈ V
45	43 44	opth	⊢ ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ↔ ( ( 1^st ‘ 𝑧 ) = ( 1^st ‘ 𝑤 ) ∧ ( 2^nd ‘ 𝑧 ) = ( 2^nd ‘ 𝑤 ) ) )
46	42 45	bitrdi	⊢ ( ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ( ℝ × ℝ ) ) → ( 𝑧 = 𝑤 ↔ ( ( 1^st ‘ 𝑧 ) = ( 1^st ‘ 𝑤 ) ∧ ( 2^nd ‘ 𝑧 ) = ( 2^nd ‘ 𝑤 ) ) ) )
47	32 40 46	3bitr4d	⊢ ( ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ( ℝ × ℝ ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ 𝑧 = 𝑤 ) )
48	47	biimpd	⊢ ( ( 𝑧 ∈ ( ℝ × ℝ ) ∧ 𝑤 ∈ ( ℝ × ℝ ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
49	48	rgen2	⊢ ∀ 𝑧 ∈ ( ℝ × ℝ ) ∀ 𝑤 ∈ ( ℝ × ℝ ) ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 )
50		dff13	⊢ ( 𝐹 : ( ℝ × ℝ ) –1-1→ ℂ ↔ ( 𝐹 : ( ℝ × ℝ ) ⟶ ℂ ∧ ∀ 𝑧 ∈ ( ℝ × ℝ ) ∀ 𝑤 ∈ ( ℝ × ℝ ) ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
51	26 49 50	mpbir2an	⊢ 𝐹 : ( ℝ × ℝ ) –1-1→ ℂ
52		cnre	⊢ ( 𝑤 ∈ ℂ → ∃ 𝑢 ∈ ℝ ∃ 𝑣 ∈ ℝ 𝑤 = ( 𝑢 + ( i · 𝑣 ) ) )
53		oveq1	⊢ ( 𝑥 = 𝑢 → ( 𝑥 + ( i · 𝑦 ) ) = ( 𝑢 + ( i · 𝑦 ) ) )
54		oveq2	⊢ ( 𝑦 = 𝑣 → ( i · 𝑦 ) = ( i · 𝑣 ) )
55	54	oveq2d	⊢ ( 𝑦 = 𝑣 → ( 𝑢 + ( i · 𝑦 ) ) = ( 𝑢 + ( i · 𝑣 ) ) )
56		ovex	⊢ ( 𝑢 + ( i · 𝑣 ) ) ∈ V
57	53 55 1 56	ovmpo	⊢ ( ( 𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ ) → ( 𝑢 𝐹 𝑣 ) = ( 𝑢 + ( i · 𝑣 ) ) )
58	57	eqeq2d	⊢ ( ( 𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ ) → ( 𝑤 = ( 𝑢 𝐹 𝑣 ) ↔ 𝑤 = ( 𝑢 + ( i · 𝑣 ) ) ) )
59	58	2rexbiia	⊢ ( ∃ 𝑢 ∈ ℝ ∃ 𝑣 ∈ ℝ 𝑤 = ( 𝑢 𝐹 𝑣 ) ↔ ∃ 𝑢 ∈ ℝ ∃ 𝑣 ∈ ℝ 𝑤 = ( 𝑢 + ( i · 𝑣 ) ) )
60	52 59	sylibr	⊢ ( 𝑤 ∈ ℂ → ∃ 𝑢 ∈ ℝ ∃ 𝑣 ∈ ℝ 𝑤 = ( 𝑢 𝐹 𝑣 ) )
61		fveq2	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
62		df-ov	⊢ ( 𝑢 𝐹 𝑣 ) = ( 𝐹 ‘ ⟨ 𝑢 , 𝑣 ⟩ )
63	61 62	eqtr4di	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝐹 ‘ 𝑧 ) = ( 𝑢 𝐹 𝑣 ) )
64	63	eqeq2d	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝑤 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑤 = ( 𝑢 𝐹 𝑣 ) ) )
65	64	rexxp	⊢ ( ∃ 𝑧 ∈ ( ℝ × ℝ ) 𝑤 = ( 𝐹 ‘ 𝑧 ) ↔ ∃ 𝑢 ∈ ℝ ∃ 𝑣 ∈ ℝ 𝑤 = ( 𝑢 𝐹 𝑣 ) )
66	60 65	sylibr	⊢ ( 𝑤 ∈ ℂ → ∃ 𝑧 ∈ ( ℝ × ℝ ) 𝑤 = ( 𝐹 ‘ 𝑧 ) )
67	66	rgen	⊢ ∀ 𝑤 ∈ ℂ ∃ 𝑧 ∈ ( ℝ × ℝ ) 𝑤 = ( 𝐹 ‘ 𝑧 )
68		dffo3	⊢ ( 𝐹 : ( ℝ × ℝ ) –onto→ ℂ ↔ ( 𝐹 : ( ℝ × ℝ ) ⟶ ℂ ∧ ∀ 𝑤 ∈ ℂ ∃ 𝑧 ∈ ( ℝ × ℝ ) 𝑤 = ( 𝐹 ‘ 𝑧 ) ) )
69	26 67 68	mpbir2an	⊢ 𝐹 : ( ℝ × ℝ ) –onto→ ℂ
70		df-f1o	⊢ ( 𝐹 : ( ℝ × ℝ ) –1-1-onto→ ℂ ↔ ( 𝐹 : ( ℝ × ℝ ) –1-1→ ℂ ∧ 𝐹 : ( ℝ × ℝ ) –onto→ ℂ ) )
71	51 69 70	mpbir2an	⊢ 𝐹 : ( ℝ × ℝ ) –1-1-onto→ ℂ

Metamath Proof Explorer

Theorem cnref1o

Proof