Theorem fsumim

Description: The imaginary part 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	fsumim	|- ( ph -> ( Im ` sum_ k e. A B ) = sum_ k e. A ( Im ` B ) )

Proof

Step	Hyp	Ref	Expression
1		fsumre.1	|- ( ph -> A e. Fin )
2		fsumre.2	|- ( ( ph /\ k e. A ) -> B e. CC )
3		imf	|- Im : CC --> RR
4		ax-resscn	|- RR C_ CC
5		fss	|- ( ( Im : CC --> RR /\ RR C_ CC ) -> Im : CC --> CC )
6	3 4 5	mp2an	|- Im : CC --> CC
7		imadd	|- ( ( x e. CC /\ y e. CC ) -> ( Im ` ( x + y ) ) = ( ( Im ` x ) + ( Im ` y ) ) )
8	1 2 6 7	fsumrelem	|- ( ph -> ( Im ` sum_ k e. A B ) = sum_ k e. A ( Im ` B ) )