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 )
8 7 adantr 
 |-  ( ( 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. )