Theorem ringidcl

Description: The unit element of a ring belongs to the base set of the ring. (Contributed by NM, 27-Aug-2011) (Revised by Mario Carneiro, 27-Dec-2014)

	Ref	Expression
Hypotheses	ringidcl.b	$$⊢B={\mathrm{Base}}_R$$
	ringidcl.u	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$

Proof

Step	Hyp	Ref	Expression
1		ringidcl.b	$$⊢B={\mathrm{Base}}_R$$
2		ringidcl.u	$$⊢\underset{\dot{}}{1}=1_R$$
3		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
4	3	ringmgp	$$⊢R\in \mathrm{Ring}\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{Ring}\to \underset{\dot{}}{1}\in B$$