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	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumre.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
Assertion	fsumcj	$$⊢\phi \to \overline{\sum _{k\in A}B}=\sum _{k\in A}\bar{B}$$

Proof

Step	Hyp	Ref	Expression
1		fsumre.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		fsumre.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
3		cjf	$$⊢*:ℂ⟶ℂ$$
4		cjadd	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to \overline{x+y}=\bar{x}+\bar{y}$$
5	1 2 3 4	fsumrelem	$$⊢\phi \to \overline{\sum _{k\in A}B}=\sum _{k\in A}\bar{B}$$