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	$$⊢B={\mathrm{Base}}_W$$
Assertion	lmodbn0	$$⊢W\in \mathrm{LMod}\to B\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		lmodbn0.b	$$⊢B={\mathrm{Base}}_W$$
2		lmodgrp	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Grp}$$
3	1	grpbn0	$$⊢W\in \mathrm{Grp}\to B\ne \varnothing$$
4	2 3	syl	$$⊢W\in \mathrm{LMod}\to B\ne \varnothing$$