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 12318 . . 3 class 2
32cslot 17214 . 2 class Slot 2
41, 3wceq 1536 1 wff +g = Slot 2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  17323  plusgid  17324  grpstr  17329  grpbaseOLD  17332  grpplusgOLD  17334  oppraddOLD  20360  sraaddgOLD  21197  zlmplusgOLD  21549  znaddOLD  21575  opsrplusgOLD  22089  tngplusgOLD  24673  ttgplusgOLD  28904  resvplusgOLD  33341  hlhilsplusOLD  41925  mnringaddgdOLD  44213
  Copyright terms: Public domain W3C validator