Description: The set of scalars in a semimodule is nonempty. (Contributed by Thierry Arnoux, 1-Apr-2018) (Proof shortened by AV, 10-Jan-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | slmdsn0.f | |- F = ( Scalar ` W ) |
|
| slmdsn0.b | |- B = ( Base ` F ) |
||
| Assertion | slmdsn0 | |- ( W e. SLMod -> B =/= (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | slmdsn0.f | |- F = ( Scalar ` W ) |
|
| 2 | slmdsn0.b | |- B = ( Base ` F ) |
|
| 3 | 1 | slmdsrg | |- ( W e. SLMod -> F e. SRing ) |
| 4 | srgmnd | |- ( F e. SRing -> F e. Mnd ) |
|
| 5 | 2 | mndbn0 | |- ( F e. Mnd -> B =/= (/) ) |
| 6 | 3 4 5 | 3syl | |- ( W e. SLMod -> B =/= (/) ) |