This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clm0vs

Description: Zero times a vector is the zero vector. Equation 1a of Kreyszig p. 51. ( lmod0vs analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 clm0vs.v 
 |-  V = ( Base ` W )
2 clm0vs.f 
 |-  F = ( Scalar ` W )
3 clm0vs.s 
 |-  .x. = ( .s ` W )
4 clm0vs.z 
 |-  .0. = ( 0g ` W )
5 2 clm0 
 |-  ( W e. CMod -> 0 = ( 0g ` F ) )
6 5 adantr 
 |-  ( ( W e. CMod /\ X e. V ) -> 0 = ( 0g ` F ) )
7 6 oveq1d 
 |-  ( ( W e. CMod /\ X e. V ) -> ( 0 .x. X ) = ( ( 0g ` F ) .x. X ) )
8 clmlmod 
 |-  ( W e. CMod -> W e. LMod )
9 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
10 1 2 3 9 4 lmod0vs 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( 0g ` F ) .x. X ) = .0. )
11 8 10 sylan 
 |-  ( ( W e. CMod /\ X e. V ) -> ( ( 0g ` F ) .x. X ) = .0. )
12 7 11 eqtrd 
 |-  ( ( W e. CMod /\ X e. V ) -> ( 0 .x. X ) = .0. )