Theorem gsummptfidmsub

Description: The difference of two group sums expressed as mappings with finite domain. (Contributed by AV, 7-Nov-2019)

	Ref	Expression
Hypotheses	gsummptfidmsub.b	$$⊢B={\mathrm{Base}}_G$$
	gsummptfidmsub.s	$$⊢\underset{\dot{}}{-}={-}_G$$
	gsummptfidmsub.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	gsummptfidmsub.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	gsummptfidmsub.c	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
	gsummptfidmsub.d	$$⊢\left(\phi \wedge x\in A\right)\to D\in B$$
	gsummptfidmsub.f	$$⊢F=\left(x\in A⟼C\right)$$
	gsummptfidmsub.h	$$⊢H=\left(x\in A⟼D\right)$$
Assertion	gsummptfidmsub	$$⊢\phi \to \underset{x\in A}{{\sum }_G}\left(C\underset{\dot{}}{-}D\right)=\left({\sum }_G,F\right)\underset{\dot{}}{-}\left({\sum }_G,H\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsummptfidmsub.b	$$⊢B={\mathrm{Base}}_G$$
2		gsummptfidmsub.s	$$⊢\underset{\dot{}}{-}={-}_G$$
3		gsummptfidmsub.g	$$⊢\phi \to G\in \mathrm{Abel}$$
4		gsummptfidmsub.a	$$⊢\phi \to A\in \mathrm{Fin}$$
5		gsummptfidmsub.c	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
6		gsummptfidmsub.d	$$⊢\left(\phi \wedge x\in A\right)\to D\in B$$
7		gsummptfidmsub.f	$$⊢F=\left(x\in A⟼C\right)$$
8		gsummptfidmsub.h	$$⊢H=\left(x\in A⟼D\right)$$
9		eqid	$$⊢0_G=0_G$$
10	7	a1i	$$⊢\phi \to F=\left(x\in A⟼C\right)$$
11	8	a1i	$$⊢\phi \to H=\left(x\in A⟼D\right)$$
12		fvexd	$$⊢\phi \to 0_G\in \mathrm{V}$$
13	7 4 5 12	fsuppmptdm	$$⊢\phi \to {finSupp}_{0_G}\left(F\right)$$
14	8 4 6 12	fsuppmptdm	$$⊢\phi \to {finSupp}_{0_G}\left(H\right)$$
15	1 9 2 3 4 5 6 10 11 13 14	gsummptfssub	$$⊢\phi \to \underset{x\in A}{{\sum }_G}\left(C\underset{\dot{}}{-}D\right)=\left({\sum }_G,F\right)\underset{\dot{}}{-}\left({\sum }_G,H\right)$$