MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sgrp Structured version   Unicode version

Definition df-sgrp 16478
Description: A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 16439), whose operation is associative. Definition in section II.1 of [Bruck] p. 23, or of an "associative magma" in definition 5 of [BourbakiAlg1] p. 4 . (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
Assertion
Ref Expression
df-sgrp  |- SGrp  =  {
g  e. Mgm  |  [. ( Base `  g )  / 
b ]. [. ( +g  `  g )  /  o ]. A. x  e.  b 
A. y  e.  b 
A. z  e.  b  ( ( x o y ) o z )  =  ( x o ( y o z ) ) }
Distinct variable group:    g, b, o, x, y, z

Detailed syntax breakdown of Definition df-sgrp
StepHypRef Expression
1 csgrp 16477 . 2  class SGrp
2 vx . . . . . . . . . . . 12  setvar  x
32cv 1436 . . . . . . . . . . 11  class  x
4 vy . . . . . . . . . . . 12  setvar  y
54cv 1436 . . . . . . . . . . 11  class  y
6 vo . . . . . . . . . . . 12  setvar  o
76cv 1436 . . . . . . . . . . 11  class  o
83, 5, 7co 6305 . . . . . . . . . 10  class  ( x o y )
9 vz . . . . . . . . . . 11  setvar  z
109cv 1436 . . . . . . . . . 10  class  z
118, 10, 7co 6305 . . . . . . . . 9  class  ( ( x o y ) o z )
125, 10, 7co 6305 . . . . . . . . . 10  class  ( y o z )
133, 12, 7co 6305 . . . . . . . . 9  class  ( x o ( y o z ) )
1411, 13wceq 1437 . . . . . . . 8  wff  ( ( x o y ) o z )  =  ( x o ( y o z ) )
15 vb . . . . . . . . 9  setvar  b
1615cv 1436 . . . . . . . 8  class  b
1714, 9, 16wral 2782 . . . . . . 7  wff  A. z  e.  b  ( (
x o y ) o z )  =  ( x o ( y o z ) )
1817, 4, 16wral 2782 . . . . . 6  wff  A. y  e.  b  A. z  e.  b  ( (
x o y ) o z )  =  ( x o ( y o z ) )
1918, 2, 16wral 2782 . . . . 5  wff  A. x  e.  b  A. y  e.  b  A. z  e.  b  ( (
x o y ) o z )  =  ( x o ( y o z ) )
20 vg . . . . . . 7  setvar  g
2120cv 1436 . . . . . 6  class  g
22 cplusg 15152 . . . . . 6  class  +g
2321, 22cfv 5601 . . . . 5  class  ( +g  `  g )
2419, 6, 23wsbc 3305 . . . 4  wff  [. ( +g  `  g )  / 
o ]. A. x  e.  b  A. y  e.  b  A. z  e.  b  ( ( x o y ) o z )  =  ( x o ( y o z ) )
25 cbs 15084 . . . . 5  class  Base
2621, 25cfv 5601 . . . 4  class  ( Base `  g )
2724, 15, 26wsbc 3305 . . 3  wff  [. ( Base `  g )  / 
b ]. [. ( +g  `  g )  /  o ]. A. x  e.  b 
A. y  e.  b 
A. z  e.  b  ( ( x o y ) o z )  =  ( x o ( y o z ) )
28 cmgm 16437 . . 3  class Mgm
2927, 20, 28crab 2786 . 2  class  { g  e. Mgm  |  [. ( Base `  g )  / 
b ]. [. ( +g  `  g )  /  o ]. A. x  e.  b 
A. y  e.  b 
A. z  e.  b  ( ( x o y ) o z )  =  ( x o ( y o z ) ) }
301, 29wceq 1437 1  wff SGrp  =  {
g  e. Mgm  |  [. ( Base `  g )  / 
b ]. [. ( +g  `  g )  /  o ]. A. x  e.  b 
A. y  e.  b 
A. z  e.  b  ( ( x o y ) o z )  =  ( x o ( y o z ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  issgrp  16479
  Copyright terms: Public domain W3C validator