Theorem fsumsub

Description: Split a finite sum over a subtraction. (Contributed by Scott Fenton, 12-Jun-2013) (Revised by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	fsumneg.1	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumneg.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
	fsumsub.3	$$⊢\left(\phi \wedge k\in A\right)\to C\in ℂ$$
Assertion	fsumsub	$$⊢\phi \to \sum _{k\in A}\left(B-C\right)=\sum _{k\in A}B-\sum _{k\in A}C$$

Proof

Step	Hyp	Ref	Expression
1		fsumneg.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		fsumneg.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
3		fsumsub.3	$$⊢\left(\phi \wedge k\in A\right)\to C\in ℂ$$
4	3	negcld	$$⊢\left(\phi \wedge k\in A\right)\to -C\in ℂ$$
5	1 2 4	fsumadd	$$⊢\phi \to \sum _{k\in A}\left(B+\left(-C\right)\right)=\sum _{k\in A}B+\sum _{k\in A}\left(-C\right)$$
6	1 3	fsumneg	$$⊢\phi \to \sum _{k\in A}\left(-C\right)=-\sum _{k\in A}C$$
7	6	oveq2d	$$⊢\phi \to \sum _{k\in A}B+\sum _{k\in A}\left(-C\right)=\sum _{k\in A}B+\left(-\sum _{k\in A}C\right)$$
8	5 7	eqtrd	$$⊢\phi \to \sum _{k\in A}\left(B+\left(-C\right)\right)=\sum _{k\in A}B+\left(-\sum _{k\in A}C\right)$$
9	2 3	negsubd	$$⊢\left(\phi \wedge k\in A\right)\to B+\left(-C\right)=B-C$$
10	9	sumeq2dv	$$⊢\phi \to \sum _{k\in A}\left(B+\left(-C\right)\right)=\sum _{k\in A}\left(B-C\right)$$
11	1 2	fsumcl	$$⊢\phi \to \sum _{k\in A}B\in ℂ$$
12	1 3	fsumcl	$$⊢\phi \to \sum _{k\in A}C\in ℂ$$
13	11 12	negsubd	$$⊢\phi \to \sum _{k\in A}B+\left(-\sum _{k\in A}C\right)=\sum _{k\in A}B-\sum _{k\in A}C$$
14	8 10 13	3eqtr3d	$$⊢\phi \to \sum _{k\in A}\left(B-C\right)=\sum _{k\in A}B-\sum _{k\in A}C$$