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

Metamath Proof Explorer

Theorem slmd1cl

Description: The ring unity 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 = Scalar (W)$
	slmd1cl.k	$⊢ K = {Base}_{F}$
	slmd1cl.u	$⊢ \underset{˙}{1} = 1_{F}$
Assertion	slmd1cl	$⊢ W \in SLMod \to \underset{˙}{1} \in K$

Proof

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