Metamath Proof Explorer


Theorem fsumcj

Description: The complex conjugate of a sum. (Contributed by Paul Chapman, 9-Nov-2007) (Revised by Mario Carneiro, 25-Jul-2014)

Ref Expression
Hypotheses fsumre.1 φ A Fin
fsumre.2 φ k A B
Assertion fsumcj φ k A B = k A B

Proof

Step Hyp Ref Expression
1 fsumre.1 φ A Fin
2 fsumre.2 φ k A B
3 cjf * :
4 cjadd x y x + y = x + y
5 1 2 3 4 fsumrelem φ k A B = k A B