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

Detailed syntax breakdown of Definition df-plusg
StepHypRef Expression
1 cplusg 17197 . 2 class +g
2 c2 12267 . . 3 class 2
32cslot 17114 . 2 class Slot 2
41, 3wceq 1542 1 wff +g = Slot 2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  17223  plusgid  17224  grpstr  17229  grpbaseOLD  17232  grpplusgOLD  17234  oppraddOLD  20160  sraaddgOLD  20795  zlmplusgOLD  21071  znaddOLD  21095  opsrplusgOLD  21609  tngplusgOLD  24154  ttgplusgOLD  28133  resvplusgOLD  32450  hlhilsplusOLD  40814  mnringaddgdOLD  42977
  Copyright terms: Public domain W3C validator