Metamath Proof Explorer


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