This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem slmdsn0

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 ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
slmdsn0.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
Assertion slmdsn0 ( 𝑊 ∈ SLMod → 𝐵 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 slmdsn0.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 slmdsn0.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
3 1 slmdsrg ⊢ ( 𝑊 ∈ SLMod → 𝐹 ∈ SRing )
4 srgmnd ⊢ ( 𝐹 ∈ SRing → 𝐹 ∈ Mnd )
5 2 mndbn0 ⊢ ( 𝐹 ∈ Mnd → 𝐵 ≠ ∅ )
6 3 4 5 3syl ⊢ ( 𝑊 ∈ SLMod → 𝐵 ≠ ∅ )