Metamath Proof Explorer


Theorem gsummulc1

Description: A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 10-Jul-2019)

Ref Expression
Hypotheses gsummulc1.b B = Base R
gsummulc1.z 0 ˙ = 0 R
gsummulc1.p + ˙ = + R
gsummulc1.t · ˙ = R
gsummulc1.r φ R Ring
gsummulc1.a φ A V
gsummulc1.y φ Y B
gsummulc1.x φ k A X B
gsummulc1.n φ finSupp 0 ˙ k A X
Assertion gsummulc1 φ R k A X · ˙ Y = R k A X · ˙ Y

Proof

Step Hyp Ref Expression
1 gsummulc1.b B = Base R
2 gsummulc1.z 0 ˙ = 0 R
3 gsummulc1.p + ˙ = + R
4 gsummulc1.t · ˙ = R
5 gsummulc1.r φ R Ring
6 gsummulc1.a φ A V
7 gsummulc1.y φ Y B
8 gsummulc1.x φ k A X B
9 gsummulc1.n φ finSupp 0 ˙ k A X
10 ringcmn R Ring R CMnd
11 5 10 syl φ R CMnd
12 ringmnd R Ring R Mnd
13 5 12 syl φ R Mnd
14 1 4 ringrghm R Ring Y B x B x · ˙ Y R GrpHom R
15 5 7 14 syl2anc φ x B x · ˙ Y R GrpHom R
16 ghmmhm x B x · ˙ Y R GrpHom R x B x · ˙ Y R MndHom R
17 15 16 syl φ x B x · ˙ Y R MndHom R
18 oveq1 x = X x · ˙ Y = X · ˙ Y
19 oveq1 x = R k A X x · ˙ Y = R k A X · ˙ Y
20 1 2 11 13 6 17 8 9 18 19 gsummhm2 φ R k A X · ˙ Y = R k A X · ˙ Y