Theorem gsummptfidmadd

Description: The sum of two group sums expressed as mappings with finite domain. (Contributed by AV, 23-Jul-2019)

	Ref	Expression
Hypotheses	gsummptfidmadd.b	$$⊢B={\mathrm{Base}}_G$$
	gsummptfidmadd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsummptfidmadd.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsummptfidmadd.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	gsummptfidmadd.c	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
	gsummptfidmadd.d	$$⊢\left(\phi \wedge x\in A\right)\to D\in B$$
	gsummptfidmadd.f	$$⊢F=\left(x\in A⟼C\right)$$
	gsummptfidmadd.h	$$⊢H=\left(x\in A⟼D\right)$$
Assertion	gsummptfidmadd	$$⊢\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		gsummptfidmadd.b	$$⊢B={\mathrm{Base}}_G$$
2		gsummptfidmadd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		gsummptfidmadd.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsummptfidmadd.a	$$⊢\phi \to A\in \mathrm{Fin}$$
5		gsummptfidmadd.c	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
6		gsummptfidmadd.d	$$⊢\left(\phi \wedge x\in A\right)\to D\in B$$
7		gsummptfidmadd.f	$$⊢F=\left(x\in A⟼C\right)$$
8		gsummptfidmadd.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	gsummptfsadd	$$⊢\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)$$