Theorem lmod0vsd

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

	Ref	Expression
Hypotheses	lmod0vsd.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lmod0vsd.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lmod0vsd.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lmod0vsd.o	⊢ 𝑂 = ( 0g ‘ 𝐹 )
	lmod0vsd.z	⊢ 0 = ( 0g ‘ 𝑊 )
	lmod0vsd.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lmod0vsd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	lmod0vsd	⊢ ( 𝜑 → ( 𝑂 · 𝑋 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		lmod0vsd.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lmod0vsd.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		lmod0vsd.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		lmod0vsd.o	⊢ 𝑂 = ( 0g ‘ 𝐹 )
5		lmod0vsd.z	⊢ 0 = ( 0g ‘ 𝑊 )
6		lmod0vsd.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
7		lmod0vsd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8	1 2 3 4 5	lmod0vs	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑂 · 𝑋 ) = 0 )
9	6 7 8	syl2anc	⊢ ( 𝜑 → ( 𝑂 · 𝑋 ) = 0 )