Metamath Proof Explorer
Description: Complex conjugate distributes over multiplication. Proposition
103.4(c) of Gleason p. 133. (Contributed by Mario Carneiro, 29May2016)


Ref 
Expression 

Hypotheses 
recld.1 
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) 


readdd.2 
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) 

Assertion 
cjmuld 
⊢ ( 𝜑 → ( ∗ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐵 ) ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

recld.1 
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) 
2 

readdd.2 
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) 
3 

cjmul 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐵 ) ) ) 
4 
1 2 3

syl2anc 
⊢ ( 𝜑 → ( ∗ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐵 ) ) ) 