# Metamath Proof Explorer

## Theorem lmodvs0

Description: Anything times the zero vector is the zero vector. Equation 1b of Kreyszig p. 51. ( hvmul0 analog.) (Contributed by NM, 12-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

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

### Proof

Step Hyp Ref Expression
1 lmodvs0.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
2 lmodvs0.s
3 lmodvs0.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
4 lmodvs0.z
5 1 lmodring ${⊢}{W}\in \mathrm{LMod}\to {F}\in \mathrm{Ring}$
6 eqid ${⊢}{\cdot }_{{F}}={\cdot }_{{F}}$
7 eqid ${⊢}{0}_{{F}}={0}_{{F}}$
8 3 6 7 ringrz ${⊢}\left({F}\in \mathrm{Ring}\wedge {X}\in {K}\right)\to {X}{\cdot }_{{F}}{0}_{{F}}={0}_{{F}}$
9 5 8 sylan ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {K}\right)\to {X}{\cdot }_{{F}}{0}_{{F}}={0}_{{F}}$
10 9 oveq1d
11 simpl ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {K}\right)\to {W}\in \mathrm{LMod}$
12 simpr ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {K}\right)\to {X}\in {K}$
13 5 adantr ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {K}\right)\to {F}\in \mathrm{Ring}$
14 3 7 ring0cl ${⊢}{F}\in \mathrm{Ring}\to {0}_{{F}}\in {K}$
15 13 14 syl ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {K}\right)\to {0}_{{F}}\in {K}$
16 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
17 16 4 lmod0vcl