This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) ) )