Theorem lmod1cl

Description: The ring unit 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	lmod1cl.f	|- F = ( Scalar ` W )
	lmod1cl.k	|- K = ( Base ` F )
	lmod1cl.u	|- .1. = ( 1r ` F )
Assertion	lmod1cl	|- ( W e. LMod -> .1. e. K )

Proof

Step	Hyp	Ref	Expression
1		lmod1cl.f	|- F = ( Scalar ` W )
2		lmod1cl.k	|- K = ( Base ` F )
3		lmod1cl.u	|- .1. = ( 1r ` F )
4	1	lmodring	|- ( W e. LMod -> F e. Ring )
5	2 3	ringidcl	|- ( F e. Ring -> .1. e. K )
6	4 5	syl	|- ( W e. LMod -> .1. e. K )