Metamath Proof Explorer

Theorem gsummulgc2

Description: A finite group sum multiplied by a constant. (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses gsummulgc1.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
gsummulgc1.t ⊢ · = ( .g ‘ 𝑀 )
gsummulgc1.r ⊢ ( 𝜑 → 𝑀 ∈ Grp )
gsummulgc1.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
gsummulgc1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
gsummulgc1.x ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ ℤ )
Assertion gsummulgc2 ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝑋 · 𝑌 ) ) ) = ( Σ 𝑘 ∈ 𝐴 𝑋 · 𝑌 ) )

Proof

Step Hyp Ref Expression
1 gsummulgc1.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 gsummulgc1.t ⊢ · = ( .g ‘ 𝑀 )
3 gsummulgc1.r ⊢ ( 𝜑 → 𝑀 ∈ Grp )
4 gsummulgc1.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
5 gsummulgc1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 gsummulgc1.x ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ ℤ )
7 zringbas ⊢ ℤ = ( Base ‘ ℤring )
8 zring0 ⊢ 0 = ( 0g ‘ ℤring )
9 zringring ⊢ ℤring ∈ Ring
10 ringcmn ⊢ ( ℤring ∈ Ring → ℤring ∈ CMnd )
11 9 10 mp1i ⊢ ( 𝜑 → ℤring ∈ CMnd )
12 3 grpmndd ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
13 eqid ⊢ ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝑌 ) ) = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝑌 ) )
14 2 13 1 mulgghm2 ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝑌 ) ) ∈ ( ℤring GrpHom 𝑀 ) )
15 3 5 14 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝑌 ) ) ∈ ( ℤring GrpHom 𝑀 ) )
16 ghmmhm ⊢ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝑌 ) ) ∈ ( ℤring GrpHom 𝑀 ) → ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝑌 ) ) ∈ ( ℤring MndHom 𝑀 ) )
17 15 16 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝑌 ) ) ∈ ( ℤring MndHom 𝑀 ) )
18 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑋 )
19 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
20 18 4 6 19 fsuppmptdm ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp 0 )
21 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 · 𝑌 ) = ( 𝑋 · 𝑌 ) )
22 oveq1 ⊢ ( 𝑥 = ( ℤring Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) → ( 𝑥 · 𝑌 ) = ( ( ℤring Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) · 𝑌 ) )
23 7 8 11 12 4 17 6 20 21 22 gsummhm2 ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝑋 · 𝑌 ) ) ) = ( ( ℤring Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) · 𝑌 ) )
24 4 6 gsumzrsum ⊢ ( 𝜑 → ( ℤring Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = Σ 𝑘 ∈ 𝐴 𝑋 )
25 24 oveq1d ⊢ ( 𝜑 → ( ( ℤring Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) · 𝑌 ) = ( Σ 𝑘 ∈ 𝐴 𝑋 · 𝑌 ) )
26 23 25 eqtrd ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝑋 · 𝑌 ) ) ) = ( Σ 𝑘 ∈ 𝐴 𝑋 · 𝑌 ) )