Metamath Proof Explorer


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=BaseR
ringidcl.u 1˙=1R
Assertion ringidcl RRing1˙B

Proof

Step Hyp Ref Expression
1 ringidcl.b B=BaseR
2 ringidcl.u 1˙=1R
3 eqid mulGrpR=mulGrpR
4 3 ringmgp RRingmulGrpRMnd
5 3 1 mgpbas B=BasemulGrpR
6 3 2 ringidval 1˙=0mulGrpR
7 5 6 mndidcl mulGrpRMnd1˙B
8 4 7 syl RRing1˙B