Description: The ring zero 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 | lmod0cl.f | |- F = ( Scalar ` W ) |
|
| lmod0cl.k | |- K = ( Base ` F ) |
||
| lmod0cl.z | |- .0. = ( 0g ` F ) |
||
| Assertion | lmod0cl | |- ( W e. LMod -> .0. e. K ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lmod0cl.f | |- F = ( Scalar ` W ) |
|
| 2 | lmod0cl.k | |- K = ( Base ` F ) |
|
| 3 | lmod0cl.z | |- .0. = ( 0g ` F ) |
|
| 4 | 1 | lmodring | |- ( W e. LMod -> F e. Ring ) |
| 5 | 2 3 | ring0cl | |- ( F e. Ring -> .0. e. K ) |
| 6 | 4 5 | syl | |- ( W e. LMod -> .0. e. K ) |