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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	slmd1cl.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	slmd1cl.u	⊢ 1 = ( 1r ‘ 𝐹 )
Assertion	slmd1cl	⊢ ( 𝑊 ∈ SLMod → 1 ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		slmd1cl.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		slmd1cl.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3		slmd1cl.u	⊢ 1 = ( 1r ‘ 𝐹 )
4	1	slmdsrg	⊢ ( 𝑊 ∈ SLMod → 𝐹 ∈ SRing )
5	2 3	srgidcl	⊢ ( 𝐹 ∈ SRing → 1 ∈ 𝐾 )
6	4 5	syl	⊢ ( 𝑊 ∈ SLMod → 1 ∈ 𝐾 )