Theorem fsumsplitf

Description: Split a sum into two parts. A version of fsumsplit using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fsumsplitf.ph	$$⊢Ⅎk\phi$$
	fsumsplitf.ab	$$⊢\phi \to A\cap B=\varnothing$$
	fsumsplitf.u	$$⊢\phi \to U=A\cup B$$
	fsumsplitf.fi	$$⊢\phi \to U\in \mathrm{Fin}$$
	fsumsplitf.c	$$⊢\left(\phi \wedge k\in U\right)\to C\in ℂ$$
Assertion	fsumsplitf	$$⊢\phi \to \sum _{k\in U}C=\sum _{k\in A}C+\sum _{k\in B}C$$

Proof

Step	Hyp	Ref	Expression
1		fsumsplitf.ph	$$⊢Ⅎk\phi$$
2		fsumsplitf.ab	$$⊢\phi \to A\cap B=\varnothing$$
3		fsumsplitf.u	$$⊢\phi \to U=A\cup B$$
4		fsumsplitf.fi	$$⊢\phi \to U\in \mathrm{Fin}$$
5		fsumsplitf.c	$$⊢\left(\phi \wedge k\in U\right)\to C\in ℂ$$
6		csbeq1a	$$⊢k=j\to C=⦋j/k⦌C$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}jC$$
8		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋j/k⦌C$$
9	6 7 8	cbvsum	$$⊢\sum _{k\in U}C=\sum _{j\in U}⦋j/k⦌C$$
10	9	a1i	$$⊢\phi \to \sum _{k\in U}C=\sum _{j\in U}⦋j/k⦌C$$
11		nfv	$$⊢Ⅎkj\in U$$
12	1 11	nfan	$$⊢Ⅎk\left(\phi \wedge j\in U\right)$$
13	8	nfel1	$$⊢Ⅎk⦋j/k⦌C\in ℂ$$
14	12 13	nfim	$$⊢Ⅎk\left(\left(\phi \wedge j\in U\right)\to ⦋j/k⦌C\in ℂ\right)$$
15		eleq1w	$$⊢k=j\to \left(k\in U\leftrightarrow j\in U\right)$$
16	15	anbi2d	$$⊢k=j\to \left(\left(\phi \wedge k\in U\right)\leftrightarrow \left(\phi \wedge j\in U\right)\right)$$
17	6	eleq1d	$$⊢k=j\to \left(C\in ℂ\leftrightarrow ⦋j/k⦌C\in ℂ\right)$$
18	16 17	imbi12d	$$⊢k=j\to \left(\left(\left(\phi \wedge k\in U\right)\to C\in ℂ\right)\leftrightarrow \left(\left(\phi \wedge j\in U\right)\to ⦋j/k⦌C\in ℂ\right)\right)$$
19	14 18 5	chvarfv	$$⊢\left(\phi \wedge j\in U\right)\to ⦋j/k⦌C\in ℂ$$
20	2 3 4 19	fsumsplit	$$⊢\phi \to \sum _{j\in U}⦋j/k⦌C=\sum _{j\in A}⦋j/k⦌C+\sum _{j\in B}⦋j/k⦌C$$
21		csbeq1a	$$⊢j=k\to ⦋j/k⦌C=⦋k/j⦌⦋j/k⦌C$$
22		csbcow	$$⊢⦋k/j⦌⦋j/k⦌C=⦋k/k⦌C$$
23		csbid	$$⊢⦋k/k⦌C=C$$
24	22 23	eqtri	$$⊢⦋k/j⦌⦋j/k⦌C=C$$
25	21 24	eqtrdi	$$⊢j=k\to ⦋j/k⦌C=C$$
26	25 8 7	cbvsum	$$⊢\sum _{j\in A}⦋j/k⦌C=\sum _{k\in A}C$$
27	25 8 7	cbvsum	$$⊢\sum _{j\in B}⦋j/k⦌C=\sum _{k\in B}C$$
28	26 27	oveq12i	$$⊢\sum _{j\in A}⦋j/k⦌C+\sum _{j\in B}⦋j/k⦌C=\sum _{k\in A}C+\sum _{k\in B}C$$
29	28	a1i	$$⊢\phi \to \sum _{j\in A}⦋j/k⦌C+\sum _{j\in B}⦋j/k⦌C=\sum _{k\in A}C+\sum _{k\in B}C$$
30	10 20 29	3eqtrd	$$⊢\phi \to \sum _{k\in U}C=\sum _{k\in A}C+\sum _{k\in B}C$$