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 𝐵 = ( Base ‘ 𝐺 )
gsummhm.z 0 = ( 0g𝐺 )
gsummhm.g ( 𝜑𝐺 ∈ CMnd )
gsummhm.h ( 𝜑𝐻 ∈ Mnd )
gsummhm.a ( 𝜑𝐴𝑉 )
gsummhm.k ( 𝜑𝐾 ∈ ( 𝐺 MndHom 𝐻 ) )
gsummhm.f ( 𝜑𝐹 : 𝐴𝐵 )
gsummhm.w ( 𝜑𝐹 finSupp 0 )
Assertion gsummhm ( 𝜑 → ( 𝐻 Σg ( 𝐾𝐹 ) ) = ( 𝐾 ‘ ( 𝐺 Σg 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 gsummhm.b 𝐵 = ( Base ‘ 𝐺 )
2 gsummhm.z 0 = ( 0g𝐺 )
3 gsummhm.g ( 𝜑𝐺 ∈ CMnd )
4 gsummhm.h ( 𝜑𝐻 ∈ Mnd )
5 gsummhm.a ( 𝜑𝐴𝑉 )
6 gsummhm.k ( 𝜑𝐾 ∈ ( 𝐺 MndHom 𝐻 ) )
7 gsummhm.f ( 𝜑𝐹 : 𝐴𝐵 )
8 gsummhm.w ( 𝜑𝐹 finSupp 0 )
9 eqid ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
10 cmnmnd ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
11 3 10 syl ( 𝜑𝐺 ∈ Mnd )
12 1 9 3 7 cntzcmnf ( 𝜑 → ran 𝐹 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝐹 ) )
13 1 9 11 4 5 6 7 12 2 8 gsumzmhm ( 𝜑 → ( 𝐻 Σg ( 𝐾𝐹 ) ) = ( 𝐾 ‘ ( 𝐺 Σg 𝐹 ) ) )