Metamath Proof Explorer


Theorem gsummulc2

Description: A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 10-Jul-2019)

Ref Expression
Hypotheses gsummulc1.b 𝐵 = ( Base ‘ 𝑅 )
gsummulc1.z 0 = ( 0g𝑅 )
gsummulc1.p + = ( +g𝑅 )
gsummulc1.t · = ( .r𝑅 )
gsummulc1.r ( 𝜑𝑅 ∈ Ring )
gsummulc1.a ( 𝜑𝐴𝑉 )
gsummulc1.y ( 𝜑𝑌𝐵 )
gsummulc1.x ( ( 𝜑𝑘𝐴 ) → 𝑋𝐵 )
gsummulc1.n ( 𝜑 → ( 𝑘𝐴𝑋 ) finSupp 0 )
Assertion gsummulc2 ( 𝜑 → ( 𝑅 Σg ( 𝑘𝐴 ↦ ( 𝑌 · 𝑋 ) ) ) = ( 𝑌 · ( 𝑅 Σg ( 𝑘𝐴𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsummulc1.b 𝐵 = ( Base ‘ 𝑅 )
2 gsummulc1.z 0 = ( 0g𝑅 )
3 gsummulc1.p + = ( +g𝑅 )
4 gsummulc1.t · = ( .r𝑅 )
5 gsummulc1.r ( 𝜑𝑅 ∈ Ring )
6 gsummulc1.a ( 𝜑𝐴𝑉 )
7 gsummulc1.y ( 𝜑𝑌𝐵 )
8 gsummulc1.x ( ( 𝜑𝑘𝐴 ) → 𝑋𝐵 )
9 gsummulc1.n ( 𝜑 → ( 𝑘𝐴𝑋 ) finSupp 0 )
10 ringcmn ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
11 5 10 syl ( 𝜑𝑅 ∈ CMnd )
12 ringmnd ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
13 5 12 syl ( 𝜑𝑅 ∈ Mnd )
14 1 4 ringlghm ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵 ) → ( 𝑥𝐵 ↦ ( 𝑌 · 𝑥 ) ) ∈ ( 𝑅 GrpHom 𝑅 ) )
15 5 7 14 syl2anc ( 𝜑 → ( 𝑥𝐵 ↦ ( 𝑌 · 𝑥 ) ) ∈ ( 𝑅 GrpHom 𝑅 ) )
16 ghmmhm ( ( 𝑥𝐵 ↦ ( 𝑌 · 𝑥 ) ) ∈ ( 𝑅 GrpHom 𝑅 ) → ( 𝑥𝐵 ↦ ( 𝑌 · 𝑥 ) ) ∈ ( 𝑅 MndHom 𝑅 ) )
17 15 16 syl ( 𝜑 → ( 𝑥𝐵 ↦ ( 𝑌 · 𝑥 ) ) ∈ ( 𝑅 MndHom 𝑅 ) )
18 oveq2 ( 𝑥 = 𝑋 → ( 𝑌 · 𝑥 ) = ( 𝑌 · 𝑋 ) )
19 oveq2 ( 𝑥 = ( 𝑅 Σg ( 𝑘𝐴𝑋 ) ) → ( 𝑌 · 𝑥 ) = ( 𝑌 · ( 𝑅 Σg ( 𝑘𝐴𝑋 ) ) ) )
20 1 2 11 13 6 17 8 9 18 19 gsummhm2 ( 𝜑 → ( 𝑅 Σg ( 𝑘𝐴 ↦ ( 𝑌 · 𝑋 ) ) ) = ( 𝑌 · ( 𝑅 Σg ( 𝑘𝐴𝑋 ) ) ) )