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

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		imf	$$⊢\Im :ℂ⟶ℝ$$
4		ax-resscn	$$⊢ℝ\subseteq ℂ$$
5		fss	$$⊢\left(\Im :ℂ⟶ℝ\wedge ℝ\subseteq ℂ\right)\to \Im :ℂ⟶ℂ$$
6	3 4 5	mp2an	$$⊢\Im :ℂ⟶ℂ$$
7		imadd	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to \Im \left(x+y\right)=\Im \left(x\right)+\Im \left(y\right)$$
8	1 2 6 7	fsumrelem	$$⊢\phi \to \Im \left(\sum _{k\in A}B\right)=\sum _{k\in A}\Im \left(B\right)$$