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

Definition df-mndOLD 16492
Description: Obsolete version of df-mnd 16488 as of 6-Feb-2020. Definition of a monoid. A monoid is a set equipped with an everywhere defined internal operation (so, a magma, see mndcl 16496), whose operation is associative (so, a semigroup, see mndass 16497) and has a two-sided neutral element (see mndid 16500). (Contributed by Mario Carneiro, 6-Jan-2015.) (New usage is discouraged.)
Assertion
Ref Expression
df-mndOLD  |- MndOLD  =  {
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-mndOLD
StepHypRef Expression
1 cmndOLD 16487 . 2  class MndOLD
2 vx . . . . . . . . . . . . 13  setvar  x
32cv 1436 . . . . . . . . . . . 12  class  x
4 vy . . . . . . . . . . . . 13  setvar  y
54cv 1436 . . . . . . . . . . . 12  class  y
6 vp . . . . . . . . . . . . 13  setvar  p
76cv 1436 . . . . . . . . . . . 12  class  p
83, 5, 7co 6305 . . . . . . . . . . 11  class  ( x p y )
9 vb . . . . . . . . . . . 12  setvar  b
109cv 1436 . . . . . . . . . . 11  class  b
118, 10wcel 1870 . . . . . . . . . 10  wff  ( x p y )  e.  b
12 vz . . . . . . . . . . . . 13  setvar  z
1312cv 1436 . . . . . . . . . . . 12  class  z
148, 13, 7co 6305 . . . . . . . . . . 11  class  ( ( x p y ) p z )
155, 13, 7co 6305 . . . . . . . . . . . 12  class  ( y p z )
163, 15, 7co 6305 . . . . . . . . . . 11  class  ( x p ( y p z ) )
1714, 16wceq 1437 . . . . . . . . . 10  wff  ( ( x p y ) p z )  =  ( x p ( y p z ) )
1811, 17wa 370 . . . . . . . . 9  wff  ( ( x p y )  e.  b  /\  (
( x p y ) p z )  =  ( x p ( y p z ) ) )
1918, 12, 10wral 2782 . . . . . . . 8  wff  A. z  e.  b  ( (
x p y )  e.  b  /\  (
( x p y ) p z )  =  ( x p ( y p z ) ) )
2019, 4, 10wral 2782 . . . . . . 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 2782 . . . . . 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  setvar  e
2322cv 1436 . . . . . . . . . . 11  class  e
2423, 3, 7co 6305 . . . . . . . . . 10  class  ( e p x )
2524, 3wceq 1437 . . . . . . . . 9  wff  ( e p x )  =  x
263, 23, 7co 6305 . . . . . . . . . 10  class  ( x p e )
2726, 3wceq 1437 . . . . . . . . 9  wff  ( x p e )  =  x
2825, 27wa 370 . . . . . . . 8  wff  ( ( e p x )  =  x  /\  (
x p e )  =  x )
2928, 2, 10wral 2782 . . . . . . 7  wff  A. x  e.  b  ( (
e p x )  =  x  /\  (
x p e )  =  x )
3029, 22, 10wrex 2783 . . . . . 6  wff  E. e  e.  b  A. x  e.  b  ( (
e p x )  =  x  /\  (
x p e )  =  x )
3121, 30wa 370 . . . . 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  setvar  g
3332cv 1436 . . . . . 6  class  g
34 cplusg 15152 . . . . . 6  class  +g
3533, 34cfv 5601 . . . . 5  class  ( +g  `  g )
3631, 6, 35wsbc 3305 . . . 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 15084 . . . . 5  class  Base
3833, 37cfv 5601 . . . 4  class  ( Base `  g )
3936, 9, 38wsbc 3305 . . 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 2414 . 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 1437 1  wff MndOLD  =  {
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 setvar class
This definition is referenced by:  ismndOLD  16493
  Copyright terms: Public domain W3C validator