Theorem gsumdifsnd

Description: Extract a summand from a finitely supported group sum. (Contributed by AV, 21-Apr-2019) (Revised by AV, 28-Jul-2019)

	Ref	Expression
Hypotheses	gsumdifsnd.b	$$⊢B={\mathrm{Base}}_G$$
	gsumdifsnd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumdifsnd.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsumdifsnd.a	$$⊢\phi \to A\in W$$
	gsumdifsnd.f	$$⊢\phi \to {finSupp}_{0_G}\left(\left(k\in A⟼X\right)\right)$$
	gsumdifsnd.e	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
	gsumdifsnd.m	$$⊢\phi \to M\in A$$
	gsumdifsnd.y	$$⊢\phi \to Y\in B$$
	gsumdifsnd.s	$$⊢\left(\phi \wedge k=M\right)\to X=Y$$
Assertion	gsumdifsnd	$$⊢\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		gsumdifsnd.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumdifsnd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		gsumdifsnd.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsumdifsnd.a	$$⊢\phi \to A\in W$$
5		gsumdifsnd.f	$$⊢\phi \to {finSupp}_{0_G}\left(\left(k\in A⟼X\right)\right)$$
6		gsumdifsnd.e	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
7		gsumdifsnd.m	$$⊢\phi \to M\in A$$
8		gsumdifsnd.y	$$⊢\phi \to Y\in B$$
9		gsumdifsnd.s	$$⊢\left(\phi \wedge k=M\right)\to X=Y$$
10		eqid	$$⊢0_G=0_G$$
11		difid	$$⊢\left\{M\right\}\setminus \left\{M\right\}=\varnothing$$
12	7	snssd	$$⊢\phi \to \left\{M\right\}\subseteq A$$
13		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\}$$
14	12 13	syl	$$⊢\phi \to \left\{M\right\}\setminus \left\{M\right\}=\left(A\setminus \left\{M\right\}\right)\cap \left\{M\right\}$$
15	11 14	syl5reqr	$$⊢\phi \to \left(A\setminus \left\{M\right\}\right)\cap \left\{M\right\}=\varnothing$$
16		difsnid	$$⊢M\in A\to \left(A\setminus \left\{M\right\}\right)\cup \left\{M\right\}=A$$
17	7 16	syl	$$⊢\phi \to \left(A\setminus \left\{M\right\}\right)\cup \left\{M\right\}=A$$
18	17	eqcomd	$$⊢\phi \to A=\left(A\setminus \left\{M\right\}\right)\cup \left\{M\right\}$$
19	1 10 2 3 4 6 5 15 18	gsumsplit2	$$⊢\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)$$
20		cmnmnd	$$⊢G\in \mathrm{CMnd}\to G\in \mathrm{Mnd}$$
21	3 20	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
22	1 21 7 8 9	gsumsnd	$$⊢\phi \to \underset{k\in \left\{M\right\}}{{\sum }_G}X=Y$$
23	22	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$$
24	19 23	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$$