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 = ( Base ` G )
	gsummhm.z	|- .0. = ( 0g ` G )
	gsummhm.g	|- ( ph -> G e. CMnd )
	gsummhm.h	|- ( ph -> H e. Mnd )
	gsummhm.a	|- ( ph -> A e. V )
	gsummhm.k	|- ( ph -> K e. ( G MndHom H ) )
	gsummhm.f	|- ( ph -> F : A --> B )
	gsummhm.w	|- ( ph -> F finSupp .0. )
Assertion	gsummhm	|- ( ph -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummhm.b	|- B = ( Base ` G )
2		gsummhm.z	|- .0. = ( 0g ` G )
3		gsummhm.g	|- ( ph -> G e. CMnd )
4		gsummhm.h	|- ( ph -> H e. Mnd )
5		gsummhm.a	|- ( ph -> A e. V )
6		gsummhm.k	|- ( ph -> K e. ( G MndHom H ) )
7		gsummhm.f	|- ( ph -> F : A --> B )
8		gsummhm.w	|- ( ph -> F finSupp .0. )
9		eqid	|- ( Cntz ` G ) = ( Cntz ` G )
10		cmnmnd	|- ( G e. CMnd -> G e. Mnd )
11	3 10	syl	|- ( ph -> G e. Mnd )
12	1 9 3 7	cntzcmnf	|- ( ph -> ran F C_ ( ( Cntz ` G ) ` ran F ) )
13	1 9 11 4 5 6 7 12 2 8	gsumzmhm	|- ( ph -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) )