Theorem lmod0vsd

Description: Zero times a vector is the zero vector. (Contributed by SN, 24-Sep-2026)

	Ref	Expression
Hypotheses	lmod0vsd.v	|- V = ( Base ` W )
	lmod0vsd.f	|- F = ( Scalar ` W )
	lmod0vsd.s	|- .x. = ( .s ` W )
	lmod0vsd.o	|- O = ( 0g ` F )
	lmod0vsd.z	|- .0. = ( 0g ` W )
	lmod0vsd.w	|- ( ph -> W e. LMod )
	lmod0vsd.x	|- ( ph -> X e. V )
Assertion	lmod0vsd	|- ( ph -> ( O .x. X ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		lmod0vsd.v	|- V = ( Base ` W )
2		lmod0vsd.f	|- F = ( Scalar ` W )
3		lmod0vsd.s	|- .x. = ( .s ` W )
4		lmod0vsd.o	|- O = ( 0g ` F )
5		lmod0vsd.z	|- .0. = ( 0g ` W )
6		lmod0vsd.w	|- ( ph -> W e. LMod )
7		lmod0vsd.x	|- ( ph -> X e. V )
8	1 2 3 4 5	lmod0vs	|- ( ( W e. LMod /\ X e. V ) -> ( O .x. X ) = .0. )
9	6 7 8	syl2anc	|- ( ph -> ( O .x. X ) = .0. )