Theorem cjmul

Description: Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of Gleason p. 133. (Contributed by NM, 29-Jul-1999) (Proof shortened by Mario Carneiro, 14-Jul-2014)

	Ref	Expression
Assertion	cjmul	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		remullem	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) ∧ ( ℑ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ∧ ( ∗ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐵 ) ) ) )
2	1	simp3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐵 ) ) )