Theorem lmod0vsd

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

	Ref	Expression
Hypotheses	lmod0vsd.v	$$⊢V={\mathrm{Base}}_W$$
	lmod0vsd.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lmod0vsd.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lmod0vsd.o	$$⊢O=0_F$$
	lmod0vsd.z	$$⊢\underset{\dot{}}{0}=0_W$$
	lmod0vsd.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lmod0vsd.x	$$⊢\phi \to X\in V$$
Assertion	lmod0vsd	$$⊢\phi \to O\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		lmod0vsd.v	$$⊢V={\mathrm{Base}}_W$$
2		lmod0vsd.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		lmod0vsd.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		lmod0vsd.o	$$⊢O=0_F$$
5		lmod0vsd.z	$$⊢\underset{\dot{}}{0}=0_W$$
6		lmod0vsd.w	$$⊢\phi \to W\in \mathrm{LMod}$$
7		lmod0vsd.x	$$⊢\phi \to X\in V$$
8	1 2 3 4 5	lmod0vs	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to O\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$
9	6 7 8	syl2anc	$$⊢\phi \to O\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$