ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ur Unicode version

Definition df-ur 13096
Description: Define the multiplicative identity, i.e., the monoid identity (df-0g 12697) of the multiplicative monoid (df-mgp 13084) 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 dfur2g 13098, 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  o. mulGrp )

Detailed syntax breakdown of Definition df-ur
StepHypRef Expression
1 cur 13095 . 2  class  1r
2 c0g 12695 . . 3  class  0g
3 cmgp 13083 . . 3  class mulGrp
42, 3ccom 4630 . 2  class  ( 0g  o. mulGrp )
51, 4wceq 1353 1  wff  1r  =  ( 0g  o. mulGrp )
Colors of variables: wff set class
This definition is referenced by:  ringidvalg  13097
  Copyright terms: Public domain W3C validator