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 → 𝐵 ≠ ∅ )