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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lmod0cl.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	lmod0cl.z	⊢ 0 = ( 0g ‘ 𝐹 )
Assertion	lmod0cl	⊢ ( 𝑊 ∈ LMod → 0 ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		lmod0cl.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		lmod0cl.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3		lmod0cl.z	⊢ 0 = ( 0g ‘ 𝐹 )
4	1	lmodring	⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Ring )
5	2 3	ring0cl	⊢ ( 𝐹 ∈ Ring → 0 ∈ 𝐾 )
6	4 5	syl	⊢ ( 𝑊 ∈ LMod → 0 ∈ 𝐾 )