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 = ( Scalar ` W )
	lmodsn0.b	|- B = ( Base ` F )
Assertion	lmodsn0	|- ( W e. LMod -> B =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		lmodsn0.f	|- F = ( Scalar ` W )
2		lmodsn0.b	|- B = ( Base ` F )
3	1	lmodfgrp	|- ( W e. LMod -> F e. Grp )
4	2	grpbn0	|- ( F e. Grp -> B =/= (/) )
5	3 4	syl	|- ( W e. LMod -> B =/= (/) )