Metamath Proof Explorer

Theorem imval

Description: The value of the imaginary part of a complex number. (Contributed by NM, 9-May-1999) (Revised by Mario Carneiro, 6-Nov-2013)

Ref Expression
Assertion imval 
|- ( A e. CC -> ( Im ` A ) = ( Re ` ( A / _i ) ) )

Proof

Step Hyp Ref Expression
1 fvoveq1 
 |-  ( x = A -> ( Re ` ( x / _i ) ) = ( Re ` ( A / _i ) ) )
2 df-im 
 |-  Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
3 fvex 
 |-  ( Re ` ( A / _i ) ) e. _V
4 1 2 3 fvmpt 
 |-  ( A e. CC -> ( Im ` A ) = ( Re ` ( A / _i ) ) )