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 ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) · 𝑌 ) )