Metamath Proof Explorer


Theorem srgsummulcr

Description: A finite semiring sum multiplied by a constant, analogous to gsummulc1 . (Contributed by AV, 23-Aug-2019)

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

Proof

Step Hyp Ref Expression
1 srgsummulcr.b 𝐵 = ( Base ‘ 𝑅 )
2 srgsummulcr.z 0 = ( 0g𝑅 )
3 srgsummulcr.p + = ( +g𝑅 )
4 srgsummulcr.t · = ( .r𝑅 )
5 srgsummulcr.r ( 𝜑𝑅 ∈ SRing )
6 srgsummulcr.a ( 𝜑𝐴𝑉 )
7 srgsummulcr.y ( 𝜑𝑌𝐵 )
8 srgsummulcr.x ( ( 𝜑𝑘𝐴 ) → 𝑋𝐵 )
9 srgsummulcr.n ( 𝜑 → ( 𝑘𝐴𝑋 ) finSupp 0 )
10 srgcmn ( 𝑅 ∈ SRing → 𝑅 ∈ CMnd )
11 5 10 syl ( 𝜑𝑅 ∈ CMnd )
12 srgmnd ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )
13 5 12 syl ( 𝜑𝑅 ∈ Mnd )
14 1 4 srgrmhm ( ( 𝑅 ∈ SRing ∧ 𝑌𝐵 ) → ( 𝑥𝐵 ↦ ( 𝑥 · 𝑌 ) ) ∈ ( 𝑅 MndHom 𝑅 ) )
15 5 7 14 syl2anc ( 𝜑 → ( 𝑥𝐵 ↦ ( 𝑥 · 𝑌 ) ) ∈ ( 𝑅 MndHom 𝑅 ) )
16 oveq1 ( 𝑥 = 𝑋 → ( 𝑥 · 𝑌 ) = ( 𝑋 · 𝑌 ) )
17 oveq1 ( 𝑥 = ( 𝑅 Σg ( 𝑘𝐴𝑋 ) ) → ( 𝑥 · 𝑌 ) = ( ( 𝑅 Σg ( 𝑘𝐴𝑋 ) ) · 𝑌 ) )
18 1 2 11 13 6 15 8 9 16 17 gsummhm2 ( 𝜑 → ( 𝑅 Σg ( 𝑘𝐴 ↦ ( 𝑋 · 𝑌 ) ) ) = ( ( 𝑅 Σg ( 𝑘𝐴𝑋 ) ) · 𝑌 ) )