Description: The base set of a left module is nonempty. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | lmodbn0.b | |- B = ( Base ` W ) |
|
| Assertion | lmodbn0 | |- ( W e. LMod -> B =/= (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lmodbn0.b | |- B = ( Base ` W ) |
|
| 2 | lmodgrp | |- ( W e. LMod -> W e. Grp ) |
|
| 3 | 1 | grpbn0 | |- ( W e. Grp -> B =/= (/) ) |
| 4 | 2 3 | syl | |- ( W e. LMod -> B =/= (/) ) |