Theorem lmodsn0

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

	Ref	Expression
Hypotheses	lmodsn0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lmodsn0.b	$$⊢B={\mathrm{Base}}_F$$
Assertion	lmodsn0	$$⊢W\in \mathrm{LMod}\to B\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		lmodsn0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		lmodsn0.b	$$⊢B={\mathrm{Base}}_F$$
3	1	lmodfgrp	$$⊢W\in \mathrm{LMod}\to F\in \mathrm{Grp}$$
4	2	grpbn0	$$⊢F\in \mathrm{Grp}\to B\ne \varnothing$$
5	3 4	syl	$$⊢W\in \mathrm{LMod}\to B\ne \varnothing$$