This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem replim

Description: Reconstruct a complex number from its real and imaginary parts. (Contributed by NM, 10-May-1999) (Revised by Mario Carneiro, 7-Nov-2013)

Ref Expression
Assertion replim 
|- ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )

Proof

Step Hyp Ref Expression
1 cnre 
 |-  ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
2 crre 
 |-  ( ( x e. RR /\ y e. RR ) -> ( Re ` ( x + ( _i x. y ) ) ) = x )
3 crim 
 |-  ( ( x e. RR /\ y e. RR ) -> ( Im ` ( x + ( _i x. y ) ) ) = y )
4 3 oveq2d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( _i x. ( Im ` ( x + ( _i x. y ) ) ) ) = ( _i x. y ) )
5 2 4 oveq12d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( Re ` ( x + ( _i x. y ) ) ) + ( _i x. ( Im ` ( x + ( _i x. y ) ) ) ) ) = ( x + ( _i x. y ) ) )
6 5 eqcomd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + ( _i x. y ) ) = ( ( Re ` ( x + ( _i x. y ) ) ) + ( _i x. ( Im ` ( x + ( _i x. y ) ) ) ) ) )
7 id 
 |-  ( A = ( x + ( _i x. y ) ) -> A = ( x + ( _i x. y ) ) )
8 fveq2 
 |-  ( A = ( x + ( _i x. y ) ) -> ( Re ` A ) = ( Re ` ( x + ( _i x. y ) ) ) )
9 fveq2 
 |-  ( A = ( x + ( _i x. y ) ) -> ( Im ` A ) = ( Im ` ( x + ( _i x. y ) ) ) )
10 9 oveq2d 
 |-  ( A = ( x + ( _i x. y ) ) -> ( _i x. ( Im ` A ) ) = ( _i x. ( Im ` ( x + ( _i x. y ) ) ) ) )
11 8 10 oveq12d 
 |-  ( A = ( x + ( _i x. y ) ) -> ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) = ( ( Re ` ( x + ( _i x. y ) ) ) + ( _i x. ( Im ` ( x + ( _i x. y ) ) ) ) ) )
12 7 11 eqeq12d 
 |-  ( A = ( x + ( _i x. y ) ) -> ( A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) <-> ( x + ( _i x. y ) ) = ( ( Re ` ( x + ( _i x. y ) ) ) + ( _i x. ( Im ` ( x + ( _i x. y ) ) ) ) ) ) )
13 6 12 syl5ibrcom 
 |-  ( ( x e. RR /\ y e. RR ) -> ( A = ( x + ( _i x. y ) ) -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) ) )
14 13 rexlimivv 
 |-  ( E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
15 1 14 syl 
 |-  ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )