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 = ( Base ` R )
	ringidcl.u	|- .1. = ( 1r ` R )
Assertion	ringidcl	|- ( R e. Ring -> .1. e. B )

Proof

Step	Hyp	Ref	Expression
1		ringidcl.b	|- B = ( Base ` R )
2		ringidcl.u	|- .1. = ( 1r ` R )
3		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
4	3	ringmgp	|- ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
5	3 1	mgpbas	|- B = ( Base ` ( mulGrp ` R ) )
6	3 2	ringidval	|- .1. = ( 0g ` ( mulGrp ` R ) )
7	5 6	mndidcl	|- ( ( mulGrp ` R ) e. Mnd -> .1. e. B )
8	4 7	syl	|- ( R e. Ring -> .1. e. B )