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

Proof

Step Hyp Ref Expression
1 gsummptmhm.b 𝐵 = ( Base ‘ 𝐺 )
2 gsummptmhm.z 0 = ( 0g𝐺 )
3 gsummptmhm.g ( 𝜑𝐺 ∈ CMnd )
4 gsummptmhm.h ( 𝜑𝐻 ∈ Mnd )
5 gsummptmhm.a ( 𝜑𝐴𝑉 )
6 gsummptmhm.k ( 𝜑𝐾 ∈ ( 𝐺 MndHom 𝐻 ) )
7 gsummptmhm.c ( ( 𝜑𝑥𝐴 ) → 𝐶𝐵 )
8 gsummptmhm.w ( 𝜑 → ( 𝑥𝐴𝐶 ) finSupp 0 )
9 eqidd ( 𝜑 → ( 𝑥𝐴𝐶 ) = ( 𝑥𝐴𝐶 ) )
10 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
11 1 10 mhmf ( 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) → 𝐾 : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
12 ffn ( 𝐾 : 𝐵 ⟶ ( Base ‘ 𝐻 ) → 𝐾 Fn 𝐵 )
13 6 11 12 3syl ( 𝜑𝐾 Fn 𝐵 )
14 dffn5 ( 𝐾 Fn 𝐵𝐾 = ( 𝑦𝐵 ↦ ( 𝐾𝑦 ) ) )
15 13 14 sylib ( 𝜑𝐾 = ( 𝑦𝐵 ↦ ( 𝐾𝑦 ) ) )
16 fveq2 ( 𝑦 = 𝐶 → ( 𝐾𝑦 ) = ( 𝐾𝐶 ) )
17 7 9 15 16 fmptco ( 𝜑 → ( 𝐾 ∘ ( 𝑥𝐴𝐶 ) ) = ( 𝑥𝐴 ↦ ( 𝐾𝐶 ) ) )
18 17 oveq2d ( 𝜑 → ( 𝐻 Σg ( 𝐾 ∘ ( 𝑥𝐴𝐶 ) ) ) = ( 𝐻 Σg ( 𝑥𝐴 ↦ ( 𝐾𝐶 ) ) ) )
19 7 fmpttd ( 𝜑 → ( 𝑥𝐴𝐶 ) : 𝐴𝐵 )
20 1 2 3 4 5 6 19 8 gsummhm ( 𝜑 → ( 𝐻 Σg ( 𝐾 ∘ ( 𝑥𝐴𝐶 ) ) ) = ( 𝐾 ‘ ( 𝐺 Σg ( 𝑥𝐴𝐶 ) ) ) )
21 18 20 eqtr3d ( 𝜑 → ( 𝐻 Σg ( 𝑥𝐴 ↦ ( 𝐾𝐶 ) ) ) = ( 𝐾 ‘ ( 𝐺 Σg ( 𝑥𝐴𝐶 ) ) ) )