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 ) ) ) )

Metamath Proof Explorer

Theorem gsummptmhm

Proof