Theorem gsumadd

Description: The sum of two group sums. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Mario Carneiro, 25-Apr-2016) (Revised by AV, 5-Jun-2019)

	Ref	Expression
Hypotheses	gsumadd.b	$$⊢B={\mathrm{Base}}_G$$
	gsumadd.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumadd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumadd.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsumadd.a	$$⊢\phi \to A\in V$$
	gsumadd.f	$$⊢\phi \to F:A⟶B$$
	gsumadd.h	$$⊢\phi \to H:A⟶B$$
	gsumadd.fn	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
	gsumadd.hn	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(H\right)$$
Assertion	gsumadd	$$⊢\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		gsumadd.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumadd.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsumadd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		gsumadd.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
5		gsumadd.a	$$⊢\phi \to A\in V$$
6		gsumadd.f	$$⊢\phi \to F:A⟶B$$
7		gsumadd.h	$$⊢\phi \to H:A⟶B$$
8		gsumadd.fn	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
9		gsumadd.hn	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(H\right)$$
10		eqid	$$⊢\mathrm{Cntz}\left(G\right)=\mathrm{Cntz}\left(G\right)$$
11		cmnmnd	$$⊢G\in \mathrm{CMnd}\to G\in \mathrm{Mnd}$$
12	4 11	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
13	1	submid	$$⊢G\in \mathrm{Mnd}\to B\in \mathrm{SubMnd}\left(G\right)$$
14	12 13	syl	$$⊢\phi \to B\in \mathrm{SubMnd}\left(G\right)$$
15		ssid	$$⊢B\subseteq B$$
16	1 10	cntzcmn	$$⊢\left(G\in \mathrm{CMnd}\wedge B\subseteq B\right)\to \mathrm{Cntz}\left(G\right)\left(B\right)=B$$
17	4 15 16	sylancl	$$⊢\phi \to \mathrm{Cntz}\left(G\right)\left(B\right)=B$$
18	15 17	sseqtrrid	$$⊢\phi \to B\subseteq \mathrm{Cntz}\left(G\right)\left(B\right)$$
19	1 2 3 10 12 5 8 9 14 18 6 7	gsumzadd	$$⊢\phi \to {\sum }_G\left(F{\underset{\dot{}}{+}}_{f}H\right)=\left({\sum }_G,F\right)\underset{\dot{}}{+}\left({\sum }_G,H\right)$$