Theorem srgsummulcr

Description: A finite semiring sum multiplied by a constant, analogous to gsummulc1 . (Contributed by AV, 23-Aug-2019)

	Ref	Expression
Hypotheses	srgsummulcr.b	|- B = ( Base ` R )
	srgsummulcr.z	|- .0. = ( 0g ` R )
	srgsummulcr.p	|- .+ = ( +g ` R )
	srgsummulcr.t	|- .x. = ( .r ` R )
	srgsummulcr.r	|- ( ph -> R e. SRing )
	srgsummulcr.a	|- ( ph -> A e. V )
	srgsummulcr.y	|- ( ph -> Y e. B )
	srgsummulcr.x	|- ( ( ph /\ k e. A ) -> X e. B )
	srgsummulcr.n	|- ( ph -> ( k e. A |-> X ) finSupp .0. )
Assertion	srgsummulcr	|- ( ph -> ( R gsum ( k e. A |-> ( X .x. Y ) ) ) = ( ( R gsum ( k e. A |-> X ) ) .x. Y ) )

Proof

Step	Hyp	Ref	Expression
1		srgsummulcr.b	|- B = ( Base ` R )
2		srgsummulcr.z	|- .0. = ( 0g ` R )
3		srgsummulcr.p	|- .+ = ( +g ` R )
4		srgsummulcr.t	|- .x. = ( .r ` R )
5		srgsummulcr.r	|- ( ph -> R e. SRing )
6		srgsummulcr.a	|- ( ph -> A e. V )
7		srgsummulcr.y	|- ( ph -> Y e. B )
8		srgsummulcr.x	|- ( ( ph /\ k e. A ) -> X e. B )
9		srgsummulcr.n	|- ( ph -> ( k e. A |-> X ) finSupp .0. )
10		srgcmn	|- ( R e. SRing -> R e. CMnd )
11	5 10	syl	|- ( ph -> R e. CMnd )
12		srgmnd	|- ( R e. SRing -> R e. Mnd )
13	5 12	syl	|- ( ph -> R e. Mnd )
14	1 4	srgrmhm	|- ( ( R e. SRing /\ Y e. B ) -> ( x e. B |-> ( x .x. Y ) ) e. ( R MndHom R ) )
15	5 7 14	syl2anc	|- ( ph -> ( x e. B |-> ( x .x. Y ) ) e. ( R MndHom R ) )
16		oveq1	|- ( x = X -> ( x .x. Y ) = ( X .x. Y ) )
17		oveq1	|- ( x = ( R gsum ( k e. A |-> X ) ) -> ( x .x. Y ) = ( ( R gsum ( k e. A |-> X ) ) .x. Y ) )
18	1 2 11 13 6 15 8 9 16 17	gsummhm2	|- ( ph -> ( R gsum ( k e. A |-> ( X .x. Y ) ) ) = ( ( R gsum ( k e. A |-> X ) ) .x. Y ) )