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	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	slmdsn0.b	$$⊢B={\mathrm{Base}}_F$$
Assertion	slmdsn0	$$⊢W\in \mathrm{SLMod}\to B\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		slmdsn0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		slmdsn0.b	$$⊢B={\mathrm{Base}}_F$$
3	1	slmdsrg	$$⊢W\in \mathrm{SLMod}\to F\in \mathrm{SRing}$$
4		srgmnd	$$⊢F\in \mathrm{SRing}\to F\in \mathrm{Mnd}$$
5	2	mndbn0	$$⊢F\in \mathrm{Mnd}\to B\ne \varnothing$$
6	3 4 5	3syl	$$⊢W\in \mathrm{SLMod}\to B\ne \varnothing$$