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	⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) = ( ℜ ‘ ( 𝐴 / i ) ) )

Proof

Step	Hyp	Ref	Expression
1		fvoveq1	⊢ ( 𝑥 = 𝐴 → ( ℜ ‘ ( 𝑥 / i ) ) = ( ℜ ‘ ( 𝐴 / i ) ) )
2		df-im	⊢ ℑ = ( 𝑥 ∈ ℂ ↦ ( ℜ ‘ ( 𝑥 / i ) ) )
3		fvex	⊢ ( ℜ ‘ ( 𝐴 / i ) ) ∈ V
4	1 2 3	fvmpt	⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) = ( ℜ ‘ ( 𝐴 / i ) ) )