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

Definition df-plusg 17310
Description: Define group operation. In the context of less restrictive structures, this operation is also called magma, semigroup or monoid operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form plusgid 17324 instead. (New usage is discouraged.)
Assertion
Ref Expression
df-plusg +g = Slot 2

Detailed syntax breakdown of Definition df-plusg
StepHypRef Expression
1 cplusg 17297 . 2 class +g
2 c2 12321 . . 3 class 2
32cslot 17218 . 2 class Slot 2
41, 3wceq 1540 1 wff +g = Slot 2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  17323  plusgid  17324  grpstr  17328  grpbaseOLD  17331  grpplusgOLD  17333  oppraddOLD  20344  sraaddgOLD  21180  zlmplusgOLD  21532  znaddOLD  21558  opsrplusgOLD  22072  tngplusgOLD  24658  ttgplusgOLD  28890  resvplusgOLD  33362  hlhilsplusOLD  41945  mnringaddgdOLD  44237
  Copyright terms: Public domain W3C validator