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

Proof

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