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 e. RR , y e. RR \|-> ( x + ( _i x. y ) ) )
	Assertion	cnref1o	\|- F : ( RR X. RR ) -1-1-onto-> CC

Proof

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

Metamath Proof Explorer

Theorem cnref1o

Proof