Description: The ring unity in a left module belongs to the set of scalars. (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 ) |
| 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 ) |