Metamath Proof Explorer

Theorem slmd0vs

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) (Revised by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Hypotheses slmd0vs.v 
|- V = ( Base ` W )
slmd0vs.f 
|- F = ( Scalar ` W )
slmd0vs.s 
|- .x. = ( .s ` W )
slmd0vs.o 
|- O = ( 0g ` F )
slmd0vs.z 
|- .0. = ( 0g ` W )
Assertion slmd0vs 
|- ( ( W e. SLMod /\ X e. V ) -> ( O .x. X ) = .0. )

Proof

Step Hyp Ref Expression
1 slmd0vs.v 
 |-  V = ( Base ` W )
2 slmd0vs.f 
 |-  F = ( Scalar ` W )
3 slmd0vs.s 
 |-  .x. = ( .s ` W )
4 slmd0vs.o 
 |-  O = ( 0g ` F )
5 slmd0vs.z 
 |-  .0. = ( 0g ` W )
6 simpl 
 |-  ( ( W e. SLMod /\ X e. V ) -> W e. SLMod )
7 eqid 
 |-  ( Base ` F ) = ( Base ` F )
8 2 7 4 slmd0cl 
 |-  ( W e. SLMod -> O e. ( Base ` F ) )
9 8 adantr 
 |-  ( ( W e. SLMod /\ X e. V ) -> O e. ( Base ` F ) )
10 simpr 
 |-  ( ( W e. SLMod /\ X e. V ) -> X e. V )
11 eqid 
 |-  ( +g ` W ) = ( +g ` W )
12 eqid 
 |-  ( +g ` F ) = ( +g ` F )
13 eqid 
 |-  ( .r ` F ) = ( .r ` F )
14 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
15 1 11 3 5 2 7 12 13 14 4 slmdlema 
 |-  ( ( W e. SLMod /\ ( O e. ( Base ` F ) /\ O e. ( Base ` F ) ) /\ ( X e. V /\ X e. V ) ) -> ( ( ( O .x. X ) e. V /\ ( O .x. ( X ( +g ` W ) X ) ) = ( ( O .x. X ) ( +g ` W ) ( O .x. X ) ) /\ ( ( O ( +g ` F ) O ) .x. X ) = ( ( O .x. X ) ( +g ` W ) ( O .x. X ) ) ) /\ ( ( ( O ( .r ` F ) O ) .x. X ) = ( O .x. ( O .x. X ) ) /\ ( ( 1r ` F ) .x. X ) = X /\ ( O .x. X ) = .0. ) ) )
16 6 9 9 10 10 15 syl122anc 
 |-  ( ( W e. SLMod /\ X e. V ) -> ( ( ( O .x. X ) e. V /\ ( O .x. ( X ( +g ` W ) X ) ) = ( ( O .x. X ) ( +g ` W ) ( O .x. X ) ) /\ ( ( O ( +g ` F ) O ) .x. X ) = ( ( O .x. X ) ( +g ` W ) ( O .x. X ) ) ) /\ ( ( ( O ( .r ` F ) O ) .x. X ) = ( O .x. ( O .x. X ) ) /\ ( ( 1r ` F ) .x. X ) = X /\ ( O .x. X ) = .0. ) ) )
17 16 simprd 
 |-  ( ( W e. SLMod /\ X e. V ) -> ( ( ( O ( .r ` F ) O ) .x. X ) = ( O .x. ( O .x. X ) ) /\ ( ( 1r ` F ) .x. X ) = X /\ ( O .x. X ) = .0. ) )
18 17 simp3d 
 |-  ( ( W e. SLMod /\ X e. V ) -> ( O .x. X ) = .0. )