Theorem gsummptfidmsplit

Description: Split a group sum expressed as mapping with a finite domain into two parts. (Contributed by AV, 23-Jul-2019)

	Ref	Expression
Hypotheses	gsummptfidmsplit.b	$$⊢B={\mathrm{Base}}_G$$
	gsummptfidmsplit.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsummptfidmsplit.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsummptfidmsplit.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	gsummptfidmsplit.y	$$⊢\left(\phi \wedge k\in A\right)\to Y\in B$$
	gsummptfidmsplit.i	$$⊢\phi \to C\cap D=\varnothing$$
	gsummptfidmsplit.u	$$⊢\phi \to A=C\cup D$$
Assertion	gsummptfidmsplit	$$⊢\phi \to \underset{k\in A}{{\sum }_G}Y=\left(\underset{k\in C}{{\sum }_G},Y\right)\underset{\dot{}}{+}\left(\underset{k\in D}{{\sum }_G},Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsummptfidmsplit.b	$$⊢B={\mathrm{Base}}_G$$
2		gsummptfidmsplit.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		gsummptfidmsplit.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsummptfidmsplit.a	$$⊢\phi \to A\in \mathrm{Fin}$$
5		gsummptfidmsplit.y	$$⊢\left(\phi \wedge k\in A\right)\to Y\in B$$
6		gsummptfidmsplit.i	$$⊢\phi \to C\cap D=\varnothing$$
7		gsummptfidmsplit.u	$$⊢\phi \to A=C\cup D$$
8		eqid	$$⊢0_G=0_G$$
9		eqid	$$⊢\left(k\in A⟼Y\right)=\left(k\in A⟼Y\right)$$
10		fvexd	$$⊢\phi \to 0_G\in \mathrm{V}$$
11	9 4 5 10	fsuppmptdm	$$⊢\phi \to {finSupp}_{0_G}\left(\left(k\in A⟼Y\right)\right)$$
12	1 8 2 3 4 5 11 6 7	gsumsplit2	$$⊢\phi \to \underset{k\in A}{{\sum }_G}Y=\left(\underset{k\in C}{{\sum }_G},Y\right)\underset{\dot{}}{+}\left(\underset{k\in D}{{\sum }_G},Y\right)$$