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 = ( 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 ) )