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={\mathrm{Base}}_R$$
	srgidcl.u	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	srgidcl	$$⊢R\in \mathrm{SRing}\to \underset{\dot{}}{1}\in B$$

Proof

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