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

Detailed syntax breakdown of Definition df-plusg
StepHypRef Expression
1 cplusg 17201 . 2 class +g
2 c2 12271 . . 3 class 2
32cslot 17118 . 2 class Slot 2
41, 3wceq 1539 1 wff +g = Slot 2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  17227  plusgid  17228  grpstr  17233  grpbaseOLD  17236  grpplusgOLD  17238  oppraddOLD  20235  sraaddgOLD  20940  zlmplusgOLD  21290  znaddOLD  21314  opsrplusgOLD  21828  tngplusgOLD  24374  ttgplusgOLD  28400  resvplusgOLD  32720  hlhilsplusOLD  41117  mnringaddgdOLD  43279
  Copyright terms: Public domain W3C validator