Metamath Proof Explorer
Description: The complex conjugate of a sum. (Contributed by Paul Chapman, 9Nov2007) (Revised by Mario Carneiro, 25Jul2014)


Ref 
Expression 

Hypotheses 
fsumre.1 
⊢ ( 𝜑 → 𝐴 ∈ Fin ) 


fsumre.2 
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) 

Assertion 
fsumcj 
⊢ ( 𝜑 → ( ∗ ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( ∗ ‘ 𝐵 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

fsumre.1 
⊢ ( 𝜑 → 𝐴 ∈ Fin ) 
2 

fsumre.2 
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) 
3 

cjf 
⊢ ∗ : ℂ ⟶ ℂ 
4 

cjadd 
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ∗ ‘ ( 𝑥 + 𝑦 ) ) = ( ( ∗ ‘ 𝑥 ) + ( ∗ ‘ 𝑦 ) ) ) 
5 
1 2 3 4

fsumrelem 
⊢ ( 𝜑 → ( ∗ ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( ∗ ‘ 𝐵 ) ) 