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. )