Description: The ring unity in a semiring left module belongs to the ring base set. (Contributed by NM, 11-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014) (Revised by Thierry Arnoux, 1-Apr-2018)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | slmd1cl.f | |- F = ( Scalar ` W ) |
|
| slmd1cl.k | |- K = ( Base ` F ) |
||
| slmd1cl.u | |- .1. = ( 1r ` F ) |
||
| Assertion | slmd1cl | |- ( W e. SLMod -> .1. e. K ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | slmd1cl.f | |- F = ( Scalar ` W ) |
|
| 2 | slmd1cl.k | |- K = ( Base ` F ) |
|
| 3 | slmd1cl.u | |- .1. = ( 1r ` F ) |
|
| 4 | 1 | slmdsrg | |- ( W e. SLMod -> F e. SRing ) |
| 5 | 2 3 | srgidcl | |- ( F e. SRing -> .1. e. K ) |
| 6 | 4 5 | syl | |- ( W e. SLMod -> .1. e. K ) |