Metamath Proof Explorer


Theorem immul2

Description: Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion immul2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( ℑ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2 immul ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) )
3 1 2 sylan ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) )
4 rere ( 𝐴 ∈ ℝ → ( ℜ ‘ 𝐴 ) = 𝐴 )
5 4 adantr ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ 𝐴 ) = 𝐴 )
6 5 oveq1d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) = ( 𝐴 · ( ℑ ‘ 𝐵 ) ) )
7 reim0 ( 𝐴 ∈ ℝ → ( ℑ ‘ 𝐴 ) = 0 )
8 7 oveq1d ( 𝐴 ∈ ℝ → ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) = ( 0 · ( ℜ ‘ 𝐵 ) ) )
9 recl ( 𝐵 ∈ ℂ → ( ℜ ‘ 𝐵 ) ∈ ℝ )
10 9 recnd ( 𝐵 ∈ ℂ → ( ℜ ‘ 𝐵 ) ∈ ℂ )
11 10 mul02d ( 𝐵 ∈ ℂ → ( 0 · ( ℜ ‘ 𝐵 ) ) = 0 )
12 8 11 sylan9eq ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) = 0 )
13 6 12 oveq12d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) = ( ( 𝐴 · ( ℑ ‘ 𝐵 ) ) + 0 ) )
14 imcl ( 𝐵 ∈ ℂ → ( ℑ ‘ 𝐵 ) ∈ ℝ )
15 14 recnd ( 𝐵 ∈ ℂ → ( ℑ ‘ 𝐵 ) ∈ ℂ )
16 mulcl ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐵 ) ∈ ℂ ) → ( 𝐴 · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
17 1 15 16 syl2an ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
18 17 addid1d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · ( ℑ ‘ 𝐵 ) ) + 0 ) = ( 𝐴 · ( ℑ ‘ 𝐵 ) ) )
19 3 13 18 3eqtrd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( ℑ ‘ 𝐵 ) ) )