Description: The ring zero in a semimodule 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 | slmd0cl.f | |- F = ( Scalar ` W ) |
|
| slmd0cl.k | |- K = ( Base ` F ) |
||
| slmd0cl.z | |- .0. = ( 0g ` F ) |
||
| Assertion | slmd0cl | |- ( W e. SLMod -> .0. e. K ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | slmd0cl.f | |- F = ( Scalar ` W ) |
|
| 2 | slmd0cl.k | |- K = ( Base ` F ) |
|
| 3 | slmd0cl.z | |- .0. = ( 0g ` F ) |
|
| 4 | 1 | slmdsrg | |- ( W e. SLMod -> F e. SRing ) |
| 5 | 2 3 | srg0cl | |- ( F e. SRing -> .0. e. K ) |
| 6 | 4 5 | syl | |- ( W e. SLMod -> .0. e. K ) |