Theorem gsummptfssub

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

	Ref	Expression
Hypotheses	gsummptfssub.b	$$⊢B={\mathrm{Base}}_G$$
	gsummptfssub.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsummptfssub.s	$$⊢\underset{\dot{}}{-}={-}_G$$
	gsummptfssub.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	gsummptfssub.a	$$⊢\phi \to A\in V$$
	gsummptfssub.c	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
	gsummptfssub.d	$$⊢\left(\phi \wedge x\in A\right)\to D\in B$$
	gsummptfssub.f	$$⊢\phi \to F=\left(x\in A⟼C\right)$$
	gsummptfssub.h	$$⊢\phi \to H=\left(x\in A⟼D\right)$$
	gsummptfssub.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
	gsummptfssub.v	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(H\right)$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		gsummptfssub.b	$$⊢B={\mathrm{Base}}_G$$
2		gsummptfssub.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsummptfssub.s	$$⊢\underset{\dot{}}{-}={-}_G$$
4		gsummptfssub.g	$$⊢\phi \to G\in \mathrm{Abel}$$
5		gsummptfssub.a	$$⊢\phi \to A\in V$$
6		gsummptfssub.c	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
7		gsummptfssub.d	$$⊢\left(\phi \wedge x\in A\right)\to D\in B$$
8		gsummptfssub.f	$$⊢\phi \to F=\left(x\in A⟼C\right)$$
9		gsummptfssub.h	$$⊢\phi \to H=\left(x\in A⟼D\right)$$
10		gsummptfssub.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
11		gsummptfssub.v	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(H\right)$$
12	5 6 7 8 9	offval2	$$⊢\phi \to F{\underset{\dot{}}{-}}_{f}H=\left(x\in A⟼C\underset{\dot{}}{-}D\right)$$
13	12	eqcomd	$$⊢\phi \to \left(x\in A⟼C\underset{\dot{}}{-}D\right)=F{\underset{\dot{}}{-}}_{f}H$$
14	13	oveq2d	$$⊢\phi \to \underset{x\in A}{{\sum }_G}\left(C\underset{\dot{}}{-}D\right)={\sum }_G\left(F{\underset{\dot{}}{-}}_{f}H\right)$$
15	8 6	fmpt3d	$$⊢\phi \to F:A⟶B$$
16	9 7	fmpt3d	$$⊢\phi \to H:A⟶B$$
17	1 2 3 4 5 15 16 10 11	gsumsub	$$⊢\phi \to {\sum }_G\left(F{\underset{\dot{}}{-}}_{f}H\right)=\left({\sum }_G,F\right)\underset{\dot{}}{-}\left({\sum }_G,H\right)$$
18	14 17	eqtrd	$$⊢\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)$$