Theorem fsumre

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