Metamath Proof Explorer


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