MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ur Structured version   Visualization version   GIF version

Definition df-ur 20199
Description: Define the multiplicative identity, i.e., the monoid identity (df-0g 17487) of the multiplicative monoid (df-mgp 20152) 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 20201, 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.)

Assertion
Ref Expression
df-ur 1r = (0g ∘ mulGrp)

Detailed syntax breakdown of Definition df-ur
StepHypRef Expression
1 cur 20198 . 2 class 1r
2 c0g 17485 . . 3 class 0g
3 cmgp 20151 . . 3 class mulGrp
42, 3ccom 5692 . 2 class (0g ∘ mulGrp)
51, 4wceq 1536 1 wff 1r = (0g ∘ mulGrp)
Colors of variables: wff setvar class
This definition is referenced by:  ringidval  20200  prds1  20336  pws1  20338
  Copyright terms: Public domain W3C validator