Metamath Proof Explorer


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