Theorem gsummhm

Description: Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 24-Apr-2016) (Revised by AV, 6-Jun-2019)

	Ref	Expression
Hypotheses	gsummhm.b	$$⊢B={\mathrm{Base}}_G$$
	gsummhm.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsummhm.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsummhm.h	$$⊢\phi \to H\in \mathrm{Mnd}$$
	gsummhm.a	$$⊢\phi \to A\in V$$
	gsummhm.k	$$⊢\phi \to K\in \left(G\mathrm{MndHom}H\right)$$
	gsummhm.f	$$⊢\phi \to F:A⟶B$$
	gsummhm.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	gsummhm	$$⊢\phi \to {\sum }_H\left(K\circ F\right)=K\left({\sum }_{G}F\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsummhm.b	$$⊢B={\mathrm{Base}}_G$$
2		gsummhm.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsummhm.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsummhm.h	$$⊢\phi \to H\in \mathrm{Mnd}$$
5		gsummhm.a	$$⊢\phi \to A\in V$$
6		gsummhm.k	$$⊢\phi \to K\in \left(G\mathrm{MndHom}H\right)$$
7		gsummhm.f	$$⊢\phi \to F:A⟶B$$
8		gsummhm.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
9		eqid	$$⊢\mathrm{Cntz}\left(G\right)=\mathrm{Cntz}\left(G\right)$$
10		cmnmnd	$$⊢G\in \mathrm{CMnd}\to G\in \mathrm{Mnd}$$
11	3 10	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
12	1 9 3 7	cntzcmnf	$$⊢\phi \to \mathrm{ran}F\subseteq \mathrm{Cntz}\left(G\right)\left(\mathrm{ran}F\right)$$
13	1 9 11 4 5 6 7 12 2 8	gsumzmhm	$$⊢\phi \to {\sum }_H\left(K\circ F\right)=K\left({\sum }_{G}F\right)$$