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	|- ( ph -> A e. Fin )
	fsumre.2	|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion	fsumcj	|- ( ph -> ( * ` sum_ k e. A B ) = sum_ k e. A ( * ` B ) )

Proof

Step	Hyp	Ref	Expression
1		fsumre.1	|- ( ph -> A e. Fin )
2		fsumre.2	|- ( ( ph /\ k e. A ) -> B e. CC )
3		cjf	|- * : CC --> CC
4		cjadd	|- ( ( x e. CC /\ y e. CC ) -> ( * ` ( x + y ) ) = ( ( * ` x ) + ( * ` y ) ) )
5	1 2 3 4	fsumrelem	|- ( ph -> ( * ` sum_ k e. A B ) = sum_ k e. A ( * ` B ) )