Metamath Proof Explorer


Definition df-im

Description: Define a function whose value is the imaginary part of a complex number. See imval for its value, imcli for its closure, and replim for its use in decomposing a complex number. (Contributed by NM, 9-May-1999)

Ref Expression
Assertion df-im ℑ = ( 𝑥 ∈ ℂ ↦ ( ℜ ‘ ( 𝑥 / i ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cim
1 vx 𝑥
2 cc
3 cre
4 1 cv 𝑥
5 cdiv /
6 ci i
7 4 6 5 co ( 𝑥 / i )
8 7 3 cfv ( ℜ ‘ ( 𝑥 / i ) )
9 1 2 8 cmpt ( 𝑥 ∈ ℂ ↦ ( ℜ ‘ ( 𝑥 / i ) ) )
10 0 9 wceq ℑ = ( 𝑥 ∈ ℂ ↦ ( ℜ ‘ ( 𝑥 / i ) ) )