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	$$⊢B={\mathrm{Base}}_R$$
	gsumvsmul.s	$$⊢S=\mathrm{Scalar}\left(R\right)$$
	gsumvsmul.k	$$⊢K={\mathrm{Base}}_S$$
	gsumvsmul.z	$$⊢\underset{\dot{}}{0}=0_R$$
	gsumvsmul.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	gsumvsmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	gsumvsmul.r	$$⊢\phi \to R\in \mathrm{LMod}$$
	gsumvsmul.a	$$⊢\phi \to A\in V$$
	gsumvsmul.x	$$⊢\phi \to X\in K$$
	gsumvsmul.y	$$⊢\left(\phi \wedge k\in A\right)\to Y\in B$$
	gsumvsmul.n	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in A⟼Y\right)\right)$$
Assertion	gsumvsmul	$$⊢\phi \to \underset{k\in A}{{\sum }_R}\left(X\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{·}\left(\underset{k\in A}{{\sum }_R},Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsumvsmul.b	$$⊢B={\mathrm{Base}}_R$$
2		gsumvsmul.s	$$⊢S=\mathrm{Scalar}\left(R\right)$$
3		gsumvsmul.k	$$⊢K={\mathrm{Base}}_S$$
4		gsumvsmul.z	$$⊢\underset{\dot{}}{0}=0_R$$
5		gsumvsmul.p	$$⊢\underset{\dot{}}{+}={+}_R$$
6		gsumvsmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
7		gsumvsmul.r	$$⊢\phi \to R\in \mathrm{LMod}$$
8		gsumvsmul.a	$$⊢\phi \to A\in V$$
9		gsumvsmul.x	$$⊢\phi \to X\in K$$
10		gsumvsmul.y	$$⊢\left(\phi \wedge k\in A\right)\to Y\in B$$
11		gsumvsmul.n	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in A⟼Y\right)\right)$$
12		lmodcmn	$$⊢R\in \mathrm{LMod}\to R\in \mathrm{CMnd}$$
13	7 12	syl	$$⊢\phi \to R\in \mathrm{CMnd}$$
14		cmnmnd	$$⊢R\in \mathrm{CMnd}\to R\in \mathrm{Mnd}$$
15	13 14	syl	$$⊢\phi \to R\in \mathrm{Mnd}$$
16	1 2 6 3	lmodvsghm	$$⊢\left(R\in \mathrm{LMod}\wedge X\in K\right)\to \left(y\in B⟼X\underset{\dot{}}{·}y\right)\in \left(R\mathrm{GrpHom}R\right)$$
17	7 9 16	syl2anc	$$⊢\phi \to \left(y\in B⟼X\underset{\dot{}}{·}y\right)\in \left(R\mathrm{GrpHom}R\right)$$
18		ghmmhm	$$⊢\left(y\in B⟼X\underset{\dot{}}{·}y\right)\in \left(R\mathrm{GrpHom}R\right)\to \left(y\in B⟼X\underset{\dot{}}{·}y\right)\in \left(R\mathrm{MndHom}R\right)$$
19	17 18	syl	$$⊢\phi \to \left(y\in B⟼X\underset{\dot{}}{·}y\right)\in \left(R\mathrm{MndHom}R\right)$$
20		oveq2	$$⊢y=Y\to X\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y$$
21		oveq2	$$⊢y=\underset{k\in A}{{\sum }_R}Y\to X\underset{\dot{}}{·}y=X\underset{\dot{}}{·}\left(\underset{k\in A}{{\sum }_R},Y\right)$$
22	1 4 13 15 8 19 10 11 20 21	gsummhm2	$$⊢\phi \to \underset{k\in A}{{\sum }_R}\left(X\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{·}\left(\underset{k\in A}{{\sum }_R},Y\right)$$