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

Detailed syntax breakdown of Definition df-plusg
StepHypRef Expression
1 cplusg 17202 . 2 class +g
2 c2 12272 . . 3 class 2
32cslot 17119 . 2 class Slot 2
41, 3wceq 1540 1 wff +g = Slot 2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  17228  plusgid  17229  grpstr  17234  grpbaseOLD  17237  grpplusgOLD  17239  oppraddOLD  20236  sraaddgOLD  20941  zlmplusgOLD  21291  znaddOLD  21315  opsrplusgOLD  21829  tngplusgOLD  24375  ttgplusgOLD  28397  resvplusgOLD  32717  hlhilsplusOLD  41118  mnringaddgdOLD  43280
  Copyright terms: Public domain W3C validator