This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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