# 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 = ( Base ` W )`
lmod0vs.f
`|- F = ( Scalar ` W )`
lmod0vs.s
`|- .x. = ( .s ` W )`
lmod0vs.o
`|- O = ( 0g ` F )`
lmod0vs.z
`|- .0. = ( 0g ` W )`
Assertion lmod0vs
`|- ( ( W e. LMod /\ X e. V ) -> ( O .x. X ) = .0. )`

### Proof

Step Hyp Ref Expression
1 lmod0vs.v
` |-  V = ( Base ` W )`
2 lmod0vs.f
` |-  F = ( Scalar ` W )`
3 lmod0vs.s
` |-  .x. = ( .s ` W )`
4 lmod0vs.o
` |-  O = ( 0g ` F )`
5 lmod0vs.z
` |-  .0. = ( 0g ` W )`
6 simpl
` |-  ( ( W e. LMod /\ X e. V ) -> W e. LMod )`
7 2 lmodring
` |-  ( W e. LMod -> F e. Ring )`
` |-  ( ( W e. LMod /\ X e. V ) -> F e. Ring )`
9 eqid
` |-  ( Base ` F ) = ( Base ` F )`
10 9 4 ring0cl
` |-  ( F e. Ring -> O e. ( Base ` F ) )`
11 8 10 syl
` |-  ( ( W e. LMod /\ X e. V ) -> O e. ( Base ` F ) )`
12 simpr
` |-  ( ( W e. LMod /\ X e. V ) -> X e. V )`
13 eqid
` |-  ( +g ` W ) = ( +g ` W )`
14 eqid
` |-  ( +g ` F ) = ( +g ` F )`
15 1 13 2 3 9 14 lmodvsdir
` |-  ( ( W e. LMod /\ ( O e. ( Base ` F ) /\ O e. ( Base ` F ) /\ X e. V ) ) -> ( ( O ( +g ` F ) O ) .x. X ) = ( ( O .x. X ) ( +g ` W ) ( O .x. X ) ) )`
16 6 11 11 12 15 syl13anc
` |-  ( ( W e. LMod /\ X e. V ) -> ( ( O ( +g ` F ) O ) .x. X ) = ( ( O .x. X ) ( +g ` W ) ( O .x. X ) ) )`
17 ringgrp
` |-  ( F e. Ring -> F e. Grp )`
18 8 17 syl
` |-  ( ( W e. LMod /\ X e. V ) -> F e. Grp )`
19 9 14 4 grplid
` |-  ( ( F e. Grp /\ O e. ( Base ` F ) ) -> ( O ( +g ` F ) O ) = O )`
20 18 11 19 syl2anc
` |-  ( ( W e. LMod /\ X e. V ) -> ( O ( +g ` F ) O ) = O )`
21 20 oveq1d
` |-  ( ( W e. LMod /\ X e. V ) -> ( ( O ( +g ` F ) O ) .x. X ) = ( O .x. X ) )`
22 16 21 eqtr3d
` |-  ( ( W e. LMod /\ X e. V ) -> ( ( O .x. X ) ( +g ` W ) ( O .x. X ) ) = ( O .x. X ) )`
23 1 2 3 9 lmodvscl
` |-  ( ( W e. LMod /\ O e. ( Base ` F ) /\ X e. V ) -> ( O .x. X ) e. V )`
24 6 11 12 23 syl3anc
` |-  ( ( W e. LMod /\ X e. V ) -> ( O .x. X ) e. V )`
25 1 13 5 lmod0vid
` |-  ( ( W e. LMod /\ ( O .x. X ) e. V ) -> ( ( ( O .x. X ) ( +g ` W ) ( O .x. X ) ) = ( O .x. X ) <-> .0. = ( O .x. X ) ) )`
26 24 25 syldan
` |-  ( ( W e. LMod /\ X e. V ) -> ( ( ( O .x. X ) ( +g ` W ) ( O .x. X ) ) = ( O .x. X ) <-> .0. = ( O .x. X ) ) )`
27 22 26 mpbid
` |-  ( ( W e. LMod /\ X e. V ) -> .0. = ( O .x. X ) )`
28 27 eqcomd
` |-  ( ( W e. LMod /\ X e. V ) -> ( O .x. X ) = .0. )`