Theorem gsumdifsndf

Description: Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019)

	Ref	Expression
Hypotheses	gsumdifsndf.k	$$⊢\underset{\_}{Ⅎ}kY$$
	gsumdifsndf.n	$$⊢Ⅎk\phi$$
	gsumdifsndf.b	$$⊢B={\mathrm{Base}}_G$$
	gsumdifsndf.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumdifsndf.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsumdifsndf.a	$$⊢\phi \to A\in W$$
	gsumdifsndf.f	$$⊢\phi \to {finSupp}_{0_G}\left(\left(k\in A⟼X\right)\right)$$
	gsumdifsndf.e	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
	gsumdifsndf.m	$$⊢\phi \to M\in A$$
	gsumdifsndf.y	$$⊢\phi \to Y\in B$$
	gsumdifsndf.s	$$⊢\left(\phi \wedge k=M\right)\to X=Y$$
Assertion	gsumdifsndf	$$⊢\phi \to \underset{k\in A}{{\sum }_G}X=\left(\underset{k\in A\setminus \left\{M\right\}}{{\sum }_G},X\right)\underset{\dot{}}{+}Y$$

Proof

Step	Hyp	Ref	Expression
1		gsumdifsndf.k	$$⊢\underset{\_}{Ⅎ}kY$$
2		gsumdifsndf.n	$$⊢Ⅎk\phi$$
3		gsumdifsndf.b	$$⊢B={\mathrm{Base}}_G$$
4		gsumdifsndf.p	$$⊢\underset{\dot{}}{+}={+}_G$$
5		gsumdifsndf.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
6		gsumdifsndf.a	$$⊢\phi \to A\in W$$
7		gsumdifsndf.f	$$⊢\phi \to {finSupp}_{0_G}\left(\left(k\in A⟼X\right)\right)$$
8		gsumdifsndf.e	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
9		gsumdifsndf.m	$$⊢\phi \to M\in A$$
10		gsumdifsndf.y	$$⊢\phi \to Y\in B$$
11		gsumdifsndf.s	$$⊢\left(\phi \wedge k=M\right)\to X=Y$$
12		eqid	$$⊢0_G=0_G$$
13	9	snssd	$$⊢\phi \to \left\{M\right\}\subseteq A$$
14		difin2	$$⊢\left\{M\right\}\subseteq A\to \left\{M\right\}\setminus \left\{M\right\}=\left(A\setminus \left\{M\right\}\right)\cap \left\{M\right\}$$
15	13 14	syl	$$⊢\phi \to \left\{M\right\}\setminus \left\{M\right\}=\left(A\setminus \left\{M\right\}\right)\cap \left\{M\right\}$$
16		difid	$$⊢\left\{M\right\}\setminus \left\{M\right\}=\varnothing$$
17	15 16	eqtr3di	$$⊢\phi \to \left(A\setminus \left\{M\right\}\right)\cap \left\{M\right\}=\varnothing$$
18		difsnid	$$⊢M\in A\to \left(A\setminus \left\{M\right\}\right)\cup \left\{M\right\}=A$$
19	9 18	syl	$$⊢\phi \to \left(A\setminus \left\{M\right\}\right)\cup \left\{M\right\}=A$$
20	19	eqcomd	$$⊢\phi \to A=\left(A\setminus \left\{M\right\}\right)\cup \left\{M\right\}$$
21	2 3 12 4 5 6 8 7 17 20	gsumsplit2f	$$⊢\phi \to \underset{k\in A}{{\sum }_G}X=\left(\underset{k\in A\setminus \left\{M\right\}}{{\sum }_G},X\right)\underset{\dot{}}{+}\left(\underset{k\in \left\{M\right\}}{{\sum }_G},X\right)$$
22		cmnmnd	$$⊢G\in \mathrm{CMnd}\to G\in \mathrm{Mnd}$$
23	5 22	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
24	3 23 9 10 11 2 1	gsumsnfd	$$⊢\phi \to \underset{k\in \left\{M\right\}}{{\sum }_G}X=Y$$
25	24	oveq2d	$$⊢\phi \to \left(\underset{k\in A\setminus \left\{M\right\}}{{\sum }_G},X\right)\underset{\dot{}}{+}\left(\underset{k\in \left\{M\right\}}{{\sum }_G},X\right)=\left(\underset{k\in A\setminus \left\{M\right\}}{{\sum }_G},X\right)\underset{\dot{}}{+}Y$$
26	21 25	eqtrd	$$⊢\phi \to \underset{k\in A}{{\sum }_G}X=\left(\underset{k\in A\setminus \left\{M\right\}}{{\sum }_G},X\right)\underset{\dot{}}{+}Y$$