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

Definition df-mnd 14361
Description: Definition of a monoid. A monoid is a set equipped with an everywhere defined internal operation (so, a magma, see mndcl 14366), whose operation is associative (so, a semigroup, see mndass 14367) and has a two-sided neutral element (see mndid 14368). (Contributed by Mario Carneiro, 6-Jan-2015.)
Assertion
Ref Expression
df-mnd  |-  Mnd  =  { g  |  [. ( Base `  g )  /  b ]. [. ( +g  `  g )  /  p ]. ( A. x  e.  b  A. y  e.  b  A. z  e.  b  ( (
x p y )  e.  b  /\  (
( x p y ) p z )  =  ( x p ( y p z ) ) )  /\  E. e  e.  b  A. x  e.  b  (
( e p x )  =  x  /\  ( x p e )  =  x ) ) }
Distinct variable group:    e, b, g, p, x, y, z

Detailed syntax breakdown of Definition df-mnd
StepHypRef Expression
1 cmnd 14355 . 2  class  Mnd
2 vx . . . . . . . . . . . . 13  set  x
32cv 1623 . . . . . . . . . . . 12  class  x
4 vy . . . . . . . . . . . . 13  set  y
54cv 1623 . . . . . . . . . . . 12  class  y
6 vp . . . . . . . . . . . . 13  set  p
76cv 1623 . . . . . . . . . . . 12  class  p
83, 5, 7co 5819 . . . . . . . . . . 11  class  ( x p y )
9 vb . . . . . . . . . . . 12  set  b
109cv 1623 . . . . . . . . . . 11  class  b
118, 10wcel 1685 . . . . . . . . . 10  wff  ( x p y )  e.  b
12 vz . . . . . . . . . . . . 13  set  z
1312cv 1623 . . . . . . . . . . . 12  class  z
148, 13, 7co 5819 . . . . . . . . . . 11  class  ( ( x p y ) p z )
155, 13, 7co 5819 . . . . . . . . . . . 12  class  ( y p z )
163, 15, 7co 5819 . . . . . . . . . . 11  class  ( x p ( y p z ) )
1714, 16wceq 1624 . . . . . . . . . 10  wff  ( ( x p y ) p z )  =  ( x p ( y p z ) )
1811, 17wa 360 . . . . . . . . 9  wff  ( ( x p y )  e.  b  /\  (
( x p y ) p z )  =  ( x p ( y p z ) ) )
1918, 12, 10wral 2544 . . . . . . . 8  wff  A. z  e.  b  ( (
x p y )  e.  b  /\  (
( x p y ) p z )  =  ( x p ( y p z ) ) )
2019, 4, 10wral 2544 . . . . . . 7  wff  A. y  e.  b  A. z  e.  b  ( (
x p y )  e.  b  /\  (
( x p y ) p z )  =  ( x p ( y p z ) ) )
2120, 2, 10wral 2544 . . . . . 6  wff  A. x  e.  b  A. y  e.  b  A. z  e.  b  ( (
x p y )  e.  b  /\  (
( x p y ) p z )  =  ( x p ( y p z ) ) )
22 ve . . . . . . . . . . . 12  set  e
2322cv 1623 . . . . . . . . . . 11  class  e
2423, 3, 7co 5819 . . . . . . . . . 10  class  ( e p x )
2524, 3wceq 1624 . . . . . . . . 9  wff  ( e p x )  =  x
263, 23, 7co 5819 . . . . . . . . . 10  class  ( x p e )
2726, 3wceq 1624 . . . . . . . . 9  wff  ( x p e )  =  x
2825, 27wa 360 . . . . . . . 8  wff  ( ( e p x )  =  x  /\  (
x p e )  =  x )
2928, 2, 10wral 2544 . . . . . . 7  wff  A. x  e.  b  ( (
e p x )  =  x  /\  (
x p e )  =  x )
3029, 22, 10wrex 2545 . . . . . 6  wff  E. e  e.  b  A. x  e.  b  ( (
e p x )  =  x  /\  (
x p e )  =  x )
3121, 30wa 360 . . . . 5  wff  ( A. x  e.  b  A. y  e.  b  A. z  e.  b  (
( x p y )  e.  b  /\  ( ( x p y ) p z )  =  ( x p ( y p z ) ) )  /\  E. e  e.  b  A. x  e.  b  ( ( e p x )  =  x  /\  ( x p e )  =  x ) )
32 vg . . . . . . 7  set  g
3332cv 1623 . . . . . 6  class  g
34 cplusg 13202 . . . . . 6  class  +g
3533, 34cfv 5221 . . . . 5  class  ( +g  `  g )
3631, 6, 35wsbc 2992 . . . 4  wff  [. ( +g  `  g )  /  p ]. ( A. x  e.  b  A. y  e.  b  A. z  e.  b  ( (
x p y )  e.  b  /\  (
( x p y ) p z )  =  ( x p ( y p z ) ) )  /\  E. e  e.  b  A. x  e.  b  (
( e p x )  =  x  /\  ( x p e )  =  x ) )
37 cbs 13142 . . . . 5  class  Base
3833, 37cfv 5221 . . . 4  class  ( Base `  g )
3936, 9, 38wsbc 2992 . . 3  wff  [. ( Base `  g )  / 
b ]. [. ( +g  `  g )  /  p ]. ( A. x  e.  b  A. y  e.  b  A. z  e.  b  ( ( x p y )  e.  b  /\  ( ( x p y ) p z )  =  ( x p ( y p z ) ) )  /\  E. e  e.  b  A. x  e.  b  (
( e p x )  =  x  /\  ( x p e )  =  x ) )
4039, 32cab 2270 . 2  class  { g  |  [. ( Base `  g )  /  b ]. [. ( +g  `  g
)  /  p ]. ( A. x  e.  b 
A. y  e.  b 
A. z  e.  b  ( ( x p y )  e.  b  /\  ( ( x p y ) p z )  =  ( x p ( y p z ) ) )  /\  E. e  e.  b  A. x  e.  b  ( (
e p x )  =  x  /\  (
x p e )  =  x ) ) }
411, 40wceq 1624 1  wff  Mnd  =  { g  |  [. ( Base `  g )  /  b ]. [. ( +g  `  g )  /  p ]. ( A. x  e.  b  A. y  e.  b  A. z  e.  b  ( (
x p y )  e.  b  /\  (
( x p y ) p z )  =  ( x p ( y p z ) ) )  /\  E. e  e.  b  A. x  e.  b  (
( e p x )  =  x  /\  ( x p e )  =  x ) ) }
Colors of variables: wff set class
This definition is referenced by:  ismnd  14363
  Copyright terms: Public domain W3C validator