Theorem lmodvs0d

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

	Ref	Expression
Hypotheses	lmodvs0d.f	|- F = ( Scalar ` W )
	lmodvs0d.k	|- K = ( Base ` F )
	lmodvs0d.s	|- .x. = ( .s ` W )
	lmodvs0d.z	|- .0. = ( 0g ` W )
	lmodvs0d.w	|- ( ph -> W e. LMod )
	lmodvs0d.x	|- ( ph -> X e. K )
Assertion	lmodvs0d	|- ( ph -> ( X .x. .0. ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		lmodvs0d.f	|- F = ( Scalar ` W )
2		lmodvs0d.k	|- K = ( Base ` F )
3		lmodvs0d.s	|- .x. = ( .s ` W )
4		lmodvs0d.z	|- .0. = ( 0g ` W )
5		lmodvs0d.w	|- ( ph -> W e. LMod )
6		lmodvs0d.x	|- ( ph -> X e. K )
7	1 3 2 4	lmodvs0	|- ( ( W e. LMod /\ X e. K ) -> ( X .x. .0. ) = .0. )
8	5 6 7	syl2anc	|- ( ph -> ( X .x. .0. ) = .0. )