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

Proof

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