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

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