Theorem gsummulc1

Description: A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 10-Jul-2019) Remove unused hypothesis. (Revised by SN, 7-Mar-2025)

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

Proof

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