Theorem slmd1cl

Description: The ring unit in a semiring left module belongs to the ring base set. (Contributed by NM, 11-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

	Ref	Expression
Hypotheses	slmd1cl.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	slmd1cl.k	$$⊢K={\mathrm{Base}}_F$$
	slmd1cl.u	$$⊢\underset{\dot{}}{1}=1_F$$
Assertion	slmd1cl	$$⊢W\in \mathrm{SLMod}\to \underset{\dot{}}{1}\in K$$

Proof

Step	Hyp	Ref	Expression
1		slmd1cl.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		slmd1cl.k	$$⊢K={\mathrm{Base}}_F$$
3		slmd1cl.u	$$⊢\underset{\dot{}}{1}=1_F$$
4	1	slmdsrg	$$⊢W\in \mathrm{SLMod}\to F\in \mathrm{SRing}$$
5	2 3	srgidcl	$$⊢F\in \mathrm{SRing}\to \underset{\dot{}}{1}\in K$$
6	4 5	syl	$$⊢W\in \mathrm{SLMod}\to \underset{\dot{}}{1}\in K$$