Metamath Proof Explorer


Theorem sgsummulcl

Description: A finite semiring sum multiplied by a constant, analogous to gsummulc2 . (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 sgsummulcl
|- ( ph -> ( R gsum ( k e. A |-> ( Y .x. X ) ) ) = ( Y .x. ( R gsum ( k e. A |-> X ) ) ) )

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 srglmhm
 |-  ( ( R e. SRing /\ Y e. B ) -> ( x e. B |-> ( Y .x. x ) ) e. ( R MndHom R ) )
15 5 7 14 syl2anc
 |-  ( ph -> ( x e. B |-> ( Y .x. x ) ) e. ( R MndHom R ) )
16 oveq2
 |-  ( x = X -> ( Y .x. x ) = ( Y .x. X ) )
17 oveq2
 |-  ( x = ( R gsum ( k e. A |-> X ) ) -> ( Y .x. x ) = ( Y .x. ( R gsum ( k e. A |-> X ) ) ) )
18 1 2 11 13 6 15 8 9 16 17 gsummhm2
 |-  ( ph -> ( R gsum ( k e. A |-> ( Y .x. X ) ) ) = ( Y .x. ( R gsum ( k e. A |-> X ) ) ) )