Metamath Proof Explorer

Theorem cnrecnv

Description: The inverse to the canonical bijection from ( RR X. RR ) to CC from cnref1o . (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypothesis cnrecnv.1 
|- F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )
Assertion cnrecnv 
|- `' F = ( z e. CC |-> <. ( Re ` z ) , ( Im ` z ) >. )

Proof

Step Hyp Ref Expression
1 cnrecnv.1 
 |-  F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )
2 1 cnref1o 
 |-  F : ( RR X. RR ) -1-1-onto-> CC
3 f1ocnv 
 |-  ( F : ( RR X. RR ) -1-1-onto-> CC -> `' F : CC -1-1-onto-> ( RR X. RR ) )
4 f1of 
 |-  ( `' F : CC -1-1-onto-> ( RR X. RR ) -> `' F : CC --> ( RR X. RR ) )
5 2 3 4 mp2b 
 |-  `' F : CC --> ( RR X. RR )
6 5 a1i 
 |-  ( T. -> `' F : CC --> ( RR X. RR ) )
7 6 feqmptd 
 |-  ( T. -> `' F = ( z e. CC |-> ( `' F ` z ) ) )
8 7 mptru 
 |-  `' F = ( z e. CC |-> ( `' F ` z ) )
9 df-ov 
 |-  ( ( Re ` z ) F ( Im ` z ) ) = ( F ` <. ( Re ` z ) , ( Im ` z ) >. )
10 recl 
 |-  ( z e. CC -> ( Re ` z ) e. RR )
11 imcl 
 |-  ( z e. CC -> ( Im ` z ) e. RR )
12 oveq1 
 |-  ( x = ( Re ` z ) -> ( x + ( _i x. y ) ) = ( ( Re ` z ) + ( _i x. y ) ) )
13 oveq2 
 |-  ( y = ( Im ` z ) -> ( _i x. y ) = ( _i x. ( Im ` z ) ) )
14 13 oveq2d 
 |-  ( y = ( Im ` z ) -> ( ( Re ` z ) + ( _i x. y ) ) = ( ( Re ` z ) + ( _i x. ( Im ` z ) ) ) )
15 ovex 
 |-  ( ( Re ` z ) + ( _i x. ( Im ` z ) ) ) e. _V
16 12 14 1 15 ovmpo 
 |-  ( ( ( Re ` z ) e. RR /\ ( Im ` z ) e. RR ) -> ( ( Re ` z ) F ( Im ` z ) ) = ( ( Re ` z ) + ( _i x. ( Im ` z ) ) ) )
17 10 11 16 syl2anc 
 |-  ( z e. CC -> ( ( Re ` z ) F ( Im ` z ) ) = ( ( Re ` z ) + ( _i x. ( Im ` z ) ) ) )
18 9 17 eqtr3id 
 |-  ( z e. CC -> ( F ` <. ( Re ` z ) , ( Im ` z ) >. ) = ( ( Re ` z ) + ( _i x. ( Im ` z ) ) ) )
19 replim 
 |-  ( z e. CC -> z = ( ( Re ` z ) + ( _i x. ( Im ` z ) ) ) )
20 18 19 eqtr4d 
 |-  ( z e. CC -> ( F ` <. ( Re ` z ) , ( Im ` z ) >. ) = z )
21 20 fveq2d 
 |-  ( z e. CC -> ( `' F ` ( F ` <. ( Re ` z ) , ( Im ` z ) >. ) ) = ( `' F ` z ) )
22 10 11 opelxpd 
 |-  ( z e. CC -> <. ( Re ` z ) , ( Im ` z ) >. e. ( RR X. RR ) )
23 f1ocnvfv1 
 |-  ( ( F : ( RR X. RR ) -1-1-onto-> CC /\ <. ( Re ` z ) , ( Im ` z ) >. e. ( RR X. RR ) ) -> ( `' F ` ( F ` <. ( Re ` z ) , ( Im ` z ) >. ) ) = <. ( Re ` z ) , ( Im ` z ) >. )
24 2 22 23 sylancr 
 |-  ( z e. CC -> ( `' F ` ( F ` <. ( Re ` z ) , ( Im ` z ) >. ) ) = <. ( Re ` z ) , ( Im ` z ) >. )
25 21 24 eqtr3d 
 |-  ( z e. CC -> ( `' F ` z ) = <. ( Re ` z ) , ( Im ` z ) >. )
26 25 mpteq2ia 
 |-  ( z e. CC |-> ( `' F ` z ) ) = ( z e. CC |-> <. ( Re ` z ) , ( Im ` z ) >. )
27 8 26 eqtri 
 |-  `' F = ( z e. CC |-> <. ( Re ` z ) , ( Im ` z ) >. )