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

Definition df-mgm 15989
Description: A magma is a set equipped with an everywhere defined internal operation. Definition 1 in [BourbakiAlg1] p. 1, or definition of a groupoid in section I.1 of [Bruck] p. 1. Note: The term "groupoid" is now widely used to refer to other objects: (small) categories all of whose morphisms are invertible, or groups with a partial function replacing the binary operation. Therefore, we will only use the term "magma" for the present notion in set.mm. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
Assertion
Ref Expression
df-mgm  |- Mgm  =  {
g  |  [. ( Base `  g )  / 
b ]. [. ( +g  `  g )  /  o ]. A. x  e.  b 
A. y  e.  b  ( x o y )  e.  b }
Distinct variable group:    g, b, o, x, y

Detailed syntax breakdown of Definition df-mgm
StepHypRef Expression
1 cmgm 15987 . 2  class Mgm
2 vx . . . . . . . . . 10  setvar  x
32cv 1398 . . . . . . . . 9  class  x
4 vy . . . . . . . . . 10  setvar  y
54cv 1398 . . . . . . . . 9  class  y
6 vo . . . . . . . . . 10  setvar  o
76cv 1398 . . . . . . . . 9  class  o
83, 5, 7co 6196 . . . . . . . 8  class  ( x o y )
9 vb . . . . . . . . 9  setvar  b
109cv 1398 . . . . . . . 8  class  b
118, 10wcel 1826 . . . . . . 7  wff  ( x o y )  e.  b
1211, 4, 10wral 2732 . . . . . 6  wff  A. y  e.  b  ( x
o y )  e.  b
1312, 2, 10wral 2732 . . . . 5  wff  A. x  e.  b  A. y  e.  b  ( x
o y )  e.  b
14 vg . . . . . . 7  setvar  g
1514cv 1398 . . . . . 6  class  g
16 cplusg 14702 . . . . . 6  class  +g
1715, 16cfv 5496 . . . . 5  class  ( +g  `  g )
1813, 6, 17wsbc 3252 . . . 4  wff  [. ( +g  `  g )  / 
o ]. A. x  e.  b  A. y  e.  b  ( x o y )  e.  b
19 cbs 14634 . . . . 5  class  Base
2015, 19cfv 5496 . . . 4  class  ( Base `  g )
2118, 9, 20wsbc 3252 . . 3  wff  [. ( Base `  g )  / 
b ]. [. ( +g  `  g )  /  o ]. A. x  e.  b 
A. y  e.  b  ( x o y )  e.  b
2221, 14cab 2367 . 2  class  { g  |  [. ( Base `  g )  /  b ]. [. ( +g  `  g
)  /  o ]. A. x  e.  b  A. y  e.  b 
( x o y )  e.  b }
231, 22wceq 1399 1  wff Mgm  =  {
g  |  [. ( Base `  g )  / 
b ]. [. ( +g  `  g )  /  o ]. A. x  e.  b 
A. y  e.  b  ( x o y )  e.  b }
Colors of variables: wff setvar class
This definition is referenced by:  ismgm  15990
  Copyright terms: Public domain W3C validator