Description: Define the multiplicative identity, i.e., the monoid identity ( df-0g ) of the multiplicative monoid ( df-mgp ) of a ring-like structure. This multiplicative identity is also called "ring unity" or "unity element".
This definition works by transferring the multiplicative operation from the .r slot to the +g slot and then looking at the element which is then the 0g element, that is an identity with respect to the operation which started out in the .r slot.
See also dfur2 , which derives the "traditional" definition as the unique element of a ring which is left- and right-neutral under multiplication. (Contributed by NM, 27-Aug-2011) (Revised by Mario Carneiro, 27-Dec-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-ur | |- 1r = ( 0g o. mulGrp ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cur | |- 1r |
|
| 1 | c0g | |- 0g |
|
| 2 | cmgp | |- mulGrp |
|
| 3 | 1 2 | ccom | |- ( 0g o. mulGrp ) |
| 4 | 0 3 | wceq | |- 1r = ( 0g o. mulGrp ) |