Theorem fsumsplit1

Description: Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fsumsplit1.kph	$$⊢Ⅎk\phi$$
	fsumsplit1.kd	$$⊢\underset{\_}{Ⅎ}kD$$
	fsumsplit1.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumsplit1.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
	fsumsplit1.c	$$⊢\phi \to C\in A$$
	fsumsplit1.bd	$$⊢k=C\to B=D$$
Assertion	fsumsplit1	$$⊢\phi \to \sum _{k\in A}B=D+\sum _{k\in A\setminus \left\{C\right\}}B$$

Proof

Step	Hyp	Ref	Expression
1		fsumsplit1.kph	$$⊢Ⅎk\phi$$
2		fsumsplit1.kd	$$⊢\underset{\_}{Ⅎ}kD$$
3		fsumsplit1.a	$$⊢\phi \to A\in \mathrm{Fin}$$
4		fsumsplit1.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
5		fsumsplit1.c	$$⊢\phi \to C\in A$$
6		fsumsplit1.bd	$$⊢k=C\to B=D$$
7		uncom	$$⊢\left(A\setminus \left\{C\right\}\right)\cup \left\{C\right\}=\left\{C\right\}\cup \left(A\setminus \left\{C\right\}\right)$$
8	7	a1i	$$⊢\phi \to \left(A\setminus \left\{C\right\}\right)\cup \left\{C\right\}=\left\{C\right\}\cup \left(A\setminus \left\{C\right\}\right)$$
9	5	snssd	$$⊢\phi \to \left\{C\right\}\subseteq A$$
10		undif	$$⊢\left\{C\right\}\subseteq A\leftrightarrow \left\{C\right\}\cup \left(A\setminus \left\{C\right\}\right)=A$$
11	9 10	sylib	$$⊢\phi \to \left\{C\right\}\cup \left(A\setminus \left\{C\right\}\right)=A$$
12		eqidd	$$⊢\phi \to A=A$$
13	8 11 12	3eqtrrd	$$⊢\phi \to A=\left(A\setminus \left\{C\right\}\right)\cup \left\{C\right\}$$
14	13	sumeq1d	$$⊢\phi \to \sum _{k\in A}B=\sum _{k\in \left(A\setminus \left\{C\right\}\right)\cup \left\{C\right\}}B$$
15		diffi	$$⊢A\in \mathrm{Fin}\to A\setminus \left\{C\right\}\in \mathrm{Fin}$$
16	3 15	syl	$$⊢\phi \to A\setminus \left\{C\right\}\in \mathrm{Fin}$$
17		neldifsnd	$$⊢\phi \to \neg C\in \left(A\setminus \left\{C\right\}\right)$$
18		simpl	$$⊢\left(\phi \wedge k\in \left(A\setminus \left\{C\right\}\right)\right)\to \phi$$
19		eldifi	$$⊢k\in \left(A\setminus \left\{C\right\}\right)\to k\in A$$
20	19	adantl	$$⊢\left(\phi \wedge k\in \left(A\setminus \left\{C\right\}\right)\right)\to k\in A$$
21	18 20 4	syl2anc	$$⊢\left(\phi \wedge k\in \left(A\setminus \left\{C\right\}\right)\right)\to B\in ℂ$$
22	2	a1i	$$⊢\phi \to \underset{\_}{Ⅎ}kD$$
23		simpr	$$⊢\left(\phi \wedge k=C\right)\to k=C$$
24	23 6	syl	$$⊢\left(\phi \wedge k=C\right)\to B=D$$
25	1 22 5 24	csbiedf	$$⊢\phi \to ⦋C/k⦌B=D$$
26	25	eqcomd	$$⊢\phi \to D=⦋C/k⦌B$$
27	5	ancli	$$⊢\phi \to \left(\phi \wedge C\in A\right)$$
28		nfcv	$$⊢\underset{\_}{Ⅎ}kC$$
29		nfv	$$⊢ℲkC\in A$$
30	1 29	nfan	$$⊢Ⅎk\left(\phi \wedge C\in A\right)$$
31	28	nfcsb1	$$⊢\underset{\_}{Ⅎ}k⦋C/k⦌B$$
32		nfcv	$$⊢\underset{\_}{Ⅎ}kℂ$$
33	31 32	nfel	$$⊢Ⅎk⦋C/k⦌B\in ℂ$$
34	30 33	nfim	$$⊢Ⅎk\left(\left(\phi \wedge C\in A\right)\to ⦋C/k⦌B\in ℂ\right)$$
35		eleq1	$$⊢k=C\to \left(k\in A\leftrightarrow C\in A\right)$$
36	35	anbi2d	$$⊢k=C\to \left(\left(\phi \wedge k\in A\right)\leftrightarrow \left(\phi \wedge C\in A\right)\right)$$
37		csbeq1a	$$⊢k=C\to B=⦋C/k⦌B$$
38	37	eleq1d	$$⊢k=C\to \left(B\in ℂ\leftrightarrow ⦋C/k⦌B\in ℂ\right)$$
39	36 38	imbi12d	$$⊢k=C\to \left(\left(\left(\phi \wedge k\in A\right)\to B\in ℂ\right)\leftrightarrow \left(\left(\phi \wedge C\in A\right)\to ⦋C/k⦌B\in ℂ\right)\right)$$
40	28 34 39 4	vtoclgf	$$⊢C\in A\to \left(\left(\phi \wedge C\in A\right)\to ⦋C/k⦌B\in ℂ\right)$$
41	5 27 40	sylc	$$⊢\phi \to ⦋C/k⦌B\in ℂ$$
42	26 41	eqeltrd	$$⊢\phi \to D\in ℂ$$
43	1 2 16 5 17 21 6 42	fsumsplitsn	$$⊢\phi \to \sum _{k\in \left(A\setminus \left\{C\right\}\right)\cup \left\{C\right\}}B=\sum _{k\in A\setminus \left\{C\right\}}B+D$$
44	1 16 21	fsumclf	$$⊢\phi \to \sum _{k\in A\setminus \left\{C\right\}}B\in ℂ$$
45	44 42	addcomd	$$⊢\phi \to \sum _{k\in A\setminus \left\{C\right\}}B+D=D+\sum _{k\in A\setminus \left\{C\right\}}B$$
46	14 43 45	3eqtrd	$$⊢\phi \to \sum _{k\in A}B=D+\sum _{k\in A\setminus \left\{C\right\}}B$$