Theorem lmod0cl

Description: The ring zero in a left module belongs to the ring base set. (Contributed by NM, 11-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lmod0cl.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lmod0cl.k	$$⊢K={\mathrm{Base}}_F$$
	lmod0cl.z	$$⊢\underset{\dot{}}{0}=0_F$$
Assertion	lmod0cl	$$⊢W\in \mathrm{LMod}\to \underset{\dot{}}{0}\in K$$

Proof

Step	Hyp	Ref	Expression
1		lmod0cl.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		lmod0cl.k	$$⊢K={\mathrm{Base}}_F$$
3		lmod0cl.z	$$⊢\underset{\dot{}}{0}=0_F$$
4	1	lmodring	$$⊢W\in \mathrm{LMod}\to F\in \mathrm{Ring}$$
5	2 3	ring0cl	$$⊢F\in \mathrm{Ring}\to \underset{\dot{}}{0}\in K$$
6	4 5	syl	$$⊢W\in \mathrm{LMod}\to \underset{\dot{}}{0}\in K$$