Theorem lmodbn0

Description: The base set of a left module is nonempty. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypothesis	lmodbn0.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
Assertion	lmodbn0	⊢ ( 𝑊 ∈ LMod → 𝐵 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		lmodbn0.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		lmodgrp	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
3	1	grpbn0	⊢ ( 𝑊 ∈ Grp → 𝐵 ≠ ∅ )
4	2 3	syl	⊢ ( 𝑊 ∈ LMod → 𝐵 ≠ ∅ )