Theorem gsummptmhm

Description: Apply a group homomorphism to a group sum expressed with a mapping. (Contributed by Thierry Arnoux, 7-Sep-2018) (Revised by AV, 8-Sep-2019)

	Ref	Expression
Hypotheses	gsummptmhm.b	|- B = ( Base ` G )
	gsummptmhm.z	|- .0. = ( 0g ` G )
	gsummptmhm.g	|- ( ph -> G e. CMnd )
	gsummptmhm.h	|- ( ph -> H e. Mnd )
	gsummptmhm.a	|- ( ph -> A e. V )
	gsummptmhm.k	|- ( ph -> K e. ( G MndHom H ) )
	gsummptmhm.c	|- ( ( ph /\ x e. A ) -> C e. B )
	gsummptmhm.w	|- ( ph -> ( x e. A |-> C ) finSupp .0. )
Assertion	gsummptmhm	|- ( ph -> ( H gsum ( x e. A |-> ( K ` C ) ) ) = ( K ` ( G gsum ( x e. A |-> C ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptmhm.b	|- B = ( Base ` G )
2		gsummptmhm.z	|- .0. = ( 0g ` G )
3		gsummptmhm.g	|- ( ph -> G e. CMnd )
4		gsummptmhm.h	|- ( ph -> H e. Mnd )
5		gsummptmhm.a	|- ( ph -> A e. V )
6		gsummptmhm.k	|- ( ph -> K e. ( G MndHom H ) )
7		gsummptmhm.c	|- ( ( ph /\ x e. A ) -> C e. B )
8		gsummptmhm.w	|- ( ph -> ( x e. A |-> C ) finSupp .0. )
9		eqidd	|- ( ph -> ( x e. A |-> C ) = ( x e. A |-> C ) )
10		eqid	|- ( Base ` H ) = ( Base ` H )
11	1 10	mhmf	|- ( K e. ( G MndHom H ) -> K : B --> ( Base ` H ) )
12		ffn	|- ( K : B --> ( Base ` H ) -> K Fn B )
13	6 11 12	3syl	|- ( ph -> K Fn B )
14		dffn5	|- ( K Fn B <-> K = ( y e. B |-> ( K ` y ) ) )
15	13 14	sylib	|- ( ph -> K = ( y e. B |-> ( K ` y ) ) )
16		fveq2	|- ( y = C -> ( K ` y ) = ( K ` C ) )
17	7 9 15 16	fmptco	|- ( ph -> ( K o. ( x e. A |-> C ) ) = ( x e. A |-> ( K ` C ) ) )
18	17	oveq2d	|- ( ph -> ( H gsum ( K o. ( x e. A |-> C ) ) ) = ( H gsum ( x e. A |-> ( K ` C ) ) ) )
19	7	fmpttd	|- ( ph -> ( x e. A |-> C ) : A --> B )
20	1 2 3 4 5 6 19 8	gsummhm	|- ( ph -> ( H gsum ( K o. ( x e. A |-> C ) ) ) = ( K ` ( G gsum ( x e. A |-> C ) ) ) )
21	18 20	eqtr3d	|- ( ph -> ( H gsum ( x e. A |-> ( K ` C ) ) ) = ( K ` ( G gsum ( x e. A |-> C ) ) ) )