This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmod0cl

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

	Ref	Expression
Hypotheses	lmod0cl.f	$⊢ F = Scalar (W)$
	lmod0cl.k	$⊢ K = {Base}_{F}$
	lmod0cl.z	$⊢ \underset{˙}{0} = 0_{F}$
Assertion	lmod0cl	$⊢ W \in LMod \to \underset{˙}{0} \in K$

Proof

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