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 = ( Base ` R )
	gsumvsmul1.s	\|- S = ( Scalar ` R )
	gsumvsmul1.k	\|- K = ( Base ` S )
	gsumvsmul1.z	\|- .0. = ( 0g ` S )
	gsumvsmul1.t	\|- .x. = ( .s ` R )
	gsumvsmul1.r	\|- ( ph -> R e. LMod )
	gsumvsmul1.1	\|- ( ph -> S e. CMnd )
	gsumvsmul1.a	\|- ( ph -> A e. V )
	gsumvsmul1.x	\|- ( ph -> Y e. B )
	gsumvsmul1.y	\|- ( ( ph /\ k e. A ) -> X e. K )
	gsumvsmul1.n	\|- ( ph -> ( k e. A \|-> X ) finSupp .0. )
Assertion	gsumvsmul1	\|- ( ph -> ( R gsum ( k e. A \|-> ( X .x. Y ) ) ) = ( ( S gsum ( k e. A \|-> X ) ) .x. Y ) )

Proof

Step	Hyp	Ref	Expression
1		gsumvsmul1.b	\|- B = ( Base ` R )
2		gsumvsmul1.s	\|- S = ( Scalar ` R )
3		gsumvsmul1.k	\|- K = ( Base ` S )
4		gsumvsmul1.z	\|- .0. = ( 0g ` S )
5		gsumvsmul1.t	\|- .x. = ( .s ` R )
6		gsumvsmul1.r	\|- ( ph -> R e. LMod )
7		gsumvsmul1.1	\|- ( ph -> S e. CMnd )
8		gsumvsmul1.a	\|- ( ph -> A e. V )
9		gsumvsmul1.x	\|- ( ph -> Y e. B )
10		gsumvsmul1.y	\|- ( ( ph /\ k e. A ) -> X e. K )
11		gsumvsmul1.n	\|- ( ph -> ( k e. A \|-> X ) finSupp .0. )
12		lmodcmn	\|- ( R e. LMod -> R e. CMnd )
13		cmnmnd	\|- ( R e. CMnd -> R e. Mnd )
14	6 12 13	3syl	\|- ( ph -> R e. Mnd )
15	1 2 5 3	lmodvslmhm	\|- ( ( R e. LMod /\ Y e. B ) -> ( x e. K \|-> ( x .x. Y ) ) e. ( S GrpHom R ) )
16	6 9 15	syl2anc	\|- ( ph -> ( x e. K \|-> ( x .x. Y ) ) e. ( S GrpHom R ) )
17		ghmmhm	\|- ( ( x e. K \|-> ( x .x. Y ) ) e. ( S GrpHom R ) -> ( x e. K \|-> ( x .x. Y ) ) e. ( S MndHom R ) )
18	16 17	syl	\|- ( ph -> ( x e. K \|-> ( x .x. Y ) ) e. ( S MndHom R ) )
19		oveq1	\|- ( x = X -> ( x .x. Y ) = ( X .x. Y ) )
20		oveq1	\|- ( x = ( S gsum ( k e. A \|-> X ) ) -> ( x .x. Y ) = ( ( S gsum ( k e. A \|-> X ) ) .x. Y ) )
21	3 4 7 14 8 18 10 11 19 20	gsummhm2	\|- ( ph -> ( R gsum ( k e. A \|-> ( X .x. Y ) ) ) = ( ( S gsum ( k e. A \|-> X ) ) .x. Y ) )

Metamath Proof Explorer

Theorem gsumvsmul1

Proof