# Metamath Proof Explorer

## Theorem lmodvsghm

Description: Scalar multiplication of the vector space by a fixed scalar is an endomorphism of the additive group of vectors. (Contributed by Mario Carneiro, 5-May-2015)

Ref Expression
Hypotheses lmodvsghm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lmodvsghm.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
lmodvsghm.s
lmodvsghm.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
Assertion lmodvsghm

### Proof

Step Hyp Ref Expression
1 lmodvsghm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lmodvsghm.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
3 lmodvsghm.s
4 lmodvsghm.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
5 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
6 lmodgrp ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{Grp}$
7 6 adantr ${⊢}\left({W}\in \mathrm{LMod}\wedge {R}\in {K}\right)\to {W}\in \mathrm{Grp}$
8 1 2 3 4 lmodvscl
9 8 3expa
10 9 fmpttd
11 1 5 2 3 4 lmodvsdi
12 11 3exp2
13 12 imp43
14 1 5 lmodvacl ${⊢}\left({W}\in \mathrm{LMod}\wedge {y}\in {V}\wedge {z}\in {V}\right)\to {y}{+}_{{W}}{z}\in {V}$
15 14 3expb ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({y}\in {V}\wedge {z}\in {V}\right)\right)\to {y}{+}_{{W}}{z}\in {V}$
16 15 adantlr ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {R}\in {K}\right)\wedge \left({y}\in {V}\wedge {z}\in {V}\right)\right)\to {y}{+}_{{W}}{z}\in {V}$
17 oveq2
18 eqid
19 ovex
20 17 18 19 fvmpt
21 16 20 syl
22 oveq2
23 ovex
24 22 18 23 fvmpt
25 oveq2
26 ovex
27 25 18 26 fvmpt
28 24 27 oveqan12d