Theorem gsumvsmul1

Description: Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc1 , since every ring is a left module over itself. (Contributed by Thierry Arnoux, 12-Jun-2023)

	Ref	Expression
Hypotheses	gsumvsmul1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	gsumvsmul1.s	⊢ 𝑆 = ( Scalar ‘ 𝑅 )
	gsumvsmul1.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	gsumvsmul1.z	⊢ 0 = ( 0g ‘ 𝑆 )
	gsumvsmul1.t	⊢ · = ( ·𝑠 ‘ 𝑅 )
	gsumvsmul1.r	⊢ ( 𝜑 → 𝑅 ∈ LMod )
	gsumvsmul1.1	⊢ ( 𝜑 → 𝑆 ∈ CMnd )
	gsumvsmul1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsumvsmul1.x	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	gsumvsmul1.y	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐾 )
	gsumvsmul1.n	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp 0 )
Assertion	gsumvsmul1	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝑋 · 𝑌 ) ) ) = ( ( 𝑆 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) · 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		gsumvsmul1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		gsumvsmul1.s	⊢ 𝑆 = ( Scalar ‘ 𝑅 )
3		gsumvsmul1.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
4		gsumvsmul1.z	⊢ 0 = ( 0g ‘ 𝑆 )
5		gsumvsmul1.t	⊢ · = ( ·𝑠 ‘ 𝑅 )
6		gsumvsmul1.r	⊢ ( 𝜑 → 𝑅 ∈ LMod )
7		gsumvsmul1.1	⊢ ( 𝜑 → 𝑆 ∈ CMnd )
8		gsumvsmul1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
9		gsumvsmul1.x	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
10		gsumvsmul1.y	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐾 )
11		gsumvsmul1.n	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp 0 )
12		lmodcmn	⊢ ( 𝑅 ∈ LMod → 𝑅 ∈ CMnd )
13		cmnmnd	⊢ ( 𝑅 ∈ CMnd → 𝑅 ∈ Mnd )
14	6 12 13	3syl	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
15	1 2 5 3	lmodvslmhm	⊢ ( ( 𝑅 ∈ LMod ∧ 𝑌 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) ∈ ( 𝑆 GrpHom 𝑅 ) )
16	6 9 15	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) ∈ ( 𝑆 GrpHom 𝑅 ) )
17		ghmmhm	⊢ ( ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) ∈ ( 𝑆 GrpHom 𝑅 ) → ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) ∈ ( 𝑆 MndHom 𝑅 ) )
18	16 17	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 𝑌 ) ) ∈ ( 𝑆 MndHom 𝑅 ) )
19		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 · 𝑌 ) = ( 𝑋 · 𝑌 ) )
20		oveq1	⊢ ( 𝑥 = ( 𝑆 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) → ( 𝑥 · 𝑌 ) = ( ( 𝑆 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) · 𝑌 ) )
21	3 4 7 14 8 18 10 11 19 20	gsummhm2	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝑋 · 𝑌 ) ) ) = ( ( 𝑆 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) · 𝑌 ) )