Theorem gsumvsmul

Description: Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc2 , since every ring is a left module over itself. (Contributed by Stefan O'Rear, 6-Feb-2015) (Revised by Mario Carneiro, 5-May-2015) (Revised by AV, 10-Jul-2019)

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

Proof

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