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

Metamath Proof Explorer

Theorem srgidcl

Description: The unity element of a semiring belongs to the base set of the semiring. (Contributed by NM, 27-Aug-2011) (Revised by Mario Carneiro, 27-Dec-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

	Ref	Expression
Hypotheses	srgidcl.b	$⊢ B = {Base}_{R}$
	srgidcl.u	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	srgidcl	$⊢ R \in SRing \to \underset{˙}{1} \in B$

Proof

Step	Hyp	Ref	Expression
1		srgidcl.b	$⊢ B = {Base}_{R}$
2		srgidcl.u	$⊢ \underset{˙}{1} = 1_{R}$
3		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
4	3	srgmgp	$⊢ R \in SRing \to {mulGrp}_{R} \in Mnd$
5	3 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
6	3 2	ringidval	$⊢ \underset{˙}{1} = 0_{{mulGrp}_{R}}$
7	5 6	mndidcl	$⊢ {mulGrp}_{R} \in Mnd \to \underset{˙}{1} \in B$
8	4 7	syl	$⊢ R \in SRing \to \underset{˙}{1} \in B$