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 17324
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 17338 instead. (New usage is discouraged.)
Assertion
Ref Expression
df-plusg +g = Slot 2

Detailed syntax breakdown of Definition df-plusg
StepHypRef Expression
1 cplusg 17311 . 2 class +g
2 c2 12348 . . 3 class 2
32cslot 17228 . 2 class Slot 2
41, 3wceq 1537 1 wff +g = Slot 2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  17337  plusgid  17338  grpstr  17343  grpbaseOLD  17346  grpplusgOLD  17348  oppraddOLD  20370  sraaddgOLD  21203  zlmplusgOLD  21555  znaddOLD  21581  opsrplusgOLD  22095  tngplusgOLD  24679  ttgplusgOLD  28908  resvplusgOLD  33327  hlhilsplusOLD  41900  mnringaddgdOLD  44187
  Copyright terms: Public domain W3C validator