# Metamath Proof Explorer

## Theorem gsummulc2

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}={\mathrm{Base}}_{{R}}$
gsummulc1.z
gsummulc1.p
gsummulc1.t
gsummulc1.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
gsummulc1.a ${⊢}{\phi }\to {A}\in {V}$
gsummulc1.y ${⊢}{\phi }\to {Y}\in {B}$
gsummulc1.x ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {X}\in {B}$
gsummulc1.n
Assertion gsummulc2

### Proof

Step Hyp Ref Expression
1 gsummulc1.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 gsummulc1.z
3 gsummulc1.p
4 gsummulc1.t
5 gsummulc1.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
6 gsummulc1.a ${⊢}{\phi }\to {A}\in {V}$
7 gsummulc1.y ${⊢}{\phi }\to {Y}\in {B}$
8 gsummulc1.x ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {X}\in {B}$
9 gsummulc1.n
10 ringcmn ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{CMnd}$
11 5 10 syl ${⊢}{\phi }\to {R}\in \mathrm{CMnd}$
12 ringmnd ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Mnd}$
13 5 12 syl ${⊢}{\phi }\to {R}\in \mathrm{Mnd}$
14 1 4 ringlghm
15 5 7 14 syl2anc
16 ghmmhm
17 15 16 syl
18 oveq2
19 oveq2
20 1 2 11 13 6 17 8 9 18 19 gsummhm2