Theorem gsummptfidmsplitres

Description: Split a group sum expressed as mapping with a finite domain into two parts using restrictions. (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$$
	gsummptfidmsplitres.f	$$⊢F=\left(k\in A⟼Y\right)$$
Assertion	gsummptfidmsplitres	$$⊢\phi \to {\sum }_{G}F=\left({\sum }_G,\left({F\upharpoonright }_C\right)\right)\underset{\dot{}}{+}\left({\sum }_G,\left({F\upharpoonright }_D\right)\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		gsummptfidmsplitres.f	$$⊢F=\left(k\in A⟼Y\right)$$
9		eqid	$$⊢0_G=0_G$$
10	5 8	fmptd	$$⊢\phi \to F:A⟶B$$
11		fvexd	$$⊢\phi \to 0_G\in \mathrm{V}$$
12	8 4 5 11	fsuppmptdm	$$⊢\phi \to {finSupp}_{0_G}\left(F\right)$$
13	1 9 2 3 4 10 12 6 7	gsumsplit	$$⊢\phi \to {\sum }_{G}F=\left({\sum }_G,\left({F\upharpoonright }_C\right)\right)\underset{\dot{}}{+}\left({\sum }_G,\left({F\upharpoonright }_D\right)\right)$$