Theorem gsummptfsadd

Description: The sum of two group sums expressed as mappings. (Contributed by AV, 4-Apr-2019) (Revised by AV, 9-Jul-2019)

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

Proof

Step	Hyp	Ref	Expression
1		gsummptfsadd.b	$$⊢B={\mathrm{Base}}_G$$
2		gsummptfsadd.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsummptfsadd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		gsummptfsadd.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
5		gsummptfsadd.a	$$⊢\phi \to A\in V$$
6		gsummptfsadd.c	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
7		gsummptfsadd.d	$$⊢\left(\phi \wedge x\in A\right)\to D\in B$$
8		gsummptfsadd.f	$$⊢\phi \to F=\left(x\in A⟼C\right)$$
9		gsummptfsadd.h	$$⊢\phi \to H=\left(x\in A⟼D\right)$$
10		gsummptfsadd.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
11		gsummptfsadd.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	gsumadd	$$⊢\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)$$