# Metamath Proof Explorer

## Theorem lmod0vs

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

Ref Expression
Hypotheses lmod0vs.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lmod0vs.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
lmod0vs.s
lmod0vs.o ${⊢}{O}={0}_{{F}}$
lmod0vs.z
Assertion lmod0vs

### Proof

Step Hyp Ref Expression
1 lmod0vs.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lmod0vs.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
3 lmod0vs.s
4 lmod0vs.o ${⊢}{O}={0}_{{F}}$
5 lmod0vs.z
6 simpl ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {W}\in \mathrm{LMod}$
7 2 lmodring ${⊢}{W}\in \mathrm{LMod}\to {F}\in \mathrm{Ring}$
8 7 adantr ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {F}\in \mathrm{Ring}$
9 eqid ${⊢}{\mathrm{Base}}_{{F}}={\mathrm{Base}}_{{F}}$
10 9 4 ring0cl ${⊢}{F}\in \mathrm{Ring}\to {O}\in {\mathrm{Base}}_{{F}}$
11 8 10 syl ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {O}\in {\mathrm{Base}}_{{F}}$
12 simpr ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {X}\in {V}$
13 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
14 eqid ${⊢}{+}_{{F}}={+}_{{F}}$
15 1 13 2 3 9 14 lmodvsdir
16 6 11 11 12 15 syl13anc
17 ringgrp ${⊢}{F}\in \mathrm{Ring}\to {F}\in \mathrm{Grp}$
18 8 17 syl ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {F}\in \mathrm{Grp}$
19 9 14 4 grplid ${⊢}\left({F}\in \mathrm{Grp}\wedge {O}\in {\mathrm{Base}}_{{F}}\right)\to {O}{+}_{{F}}{O}={O}$
20 18 11 19 syl2anc ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {O}{+}_{{F}}{O}={O}$
21 20 oveq1d
22 16 21 eqtr3d
23 1 2 3 9 lmodvscl
24 6 11 12 23 syl3anc
25 1 13 5 lmod0vid
26 24 25 syldan
27 22 26 mpbid
28 27 eqcomd