Theorem gsummptfidmadd2

Description: The sum of two group sums expressed as mappings with finite domain, using a function operation. (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	gsummptfidmadd2	$$⊢\phi \to {\sum }_G\left(F{\underset{\dot{}}{+}}_{f}H\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	7	a1i	$$⊢\phi \to F=\left(x\in A⟼C\right)$$
10	8	a1i	$$⊢\phi \to H=\left(x\in A⟼D\right)$$
11	4 5 6 9 10	offval2	$$⊢\phi \to F{\underset{\dot{}}{+}}_{f}H=\left(x\in A⟼C\underset{\dot{}}{+}D\right)$$
12	11	oveq2d	$$⊢\phi \to {\sum }_G\left(F{\underset{\dot{}}{+}}_{f}H\right)=\underset{x\in A}{{\sum }_G}\left(C\underset{\dot{}}{+}D\right)$$
13	1 2 3 4 5 6 7 8	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)$$
14	12 13	eqtrd	$$⊢\phi \to {\sum }_G\left(F{\underset{\dot{}}{+}}_{f}H\right)=\left({\sum }_G,F\right)\underset{\dot{}}{+}\left({\sum }_G,H\right)$$