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

Definition df-mndOLD 16124
Description: Obsolete version of df-mnd 16120 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 16128), whose operation is associative (so, a semigroup, see mndass 16129) and has a two-sided neutral element (see mndid 16132). (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 16119 . 2  class MndOLD
2 vx . . . . . . . . . . . . 13  setvar  x
32cv 1397 . . . . . . . . . . . 12  class  x
4 vy . . . . . . . . . . . . 13  setvar  y
54cv 1397 . . . . . . . . . . . 12  class  y
6 vp . . . . . . . . . . . . 13  setvar  p
76cv 1397 . . . . . . . . . . . 12  class  p
83, 5, 7co 6270 . . . . . . . . . . 11  class  ( x p y )
9 vb . . . . . . . . . . . 12  setvar  b
109cv 1397 . . . . . . . . . . 11  class  b
118, 10wcel 1823 . . . . . . . . . 10  wff  ( x p y )  e.  b
12 vz . . . . . . . . . . . . 13  setvar  z
1312cv 1397 . . . . . . . . . . . 12  class  z
148, 13, 7co 6270 . . . . . . . . . . 11  class  ( ( x p y ) p z )
155, 13, 7co 6270 . . . . . . . . . . . 12  class  ( y p z )
163, 15, 7co 6270 . . . . . . . . . . 11  class  ( x p ( y p z ) )
1714, 16wceq 1398 . . . . . . . . . 10  wff  ( ( x p y ) p z )  =  ( x p ( y p z ) )
1811, 17wa 367 . . . . . . . . 9  wff  ( ( x p y )  e.  b  /\  (
( x p y ) p z )  =  ( x p ( y p z ) ) )
1918, 12, 10wral 2804 . . . . . . . 8  wff  A. z  e.  b  ( (
x p y )  e.  b  /\  (
( x p y ) p z )  =  ( x p ( y p z ) ) )
2019, 4, 10wral 2804 . . . . . . 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 2804 . . . . . 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 1397 . . . . . . . . . . 11  class  e
2423, 3, 7co 6270 . . . . . . . . . 10  class  ( e p x )
2524, 3wceq 1398 . . . . . . . . 9  wff  ( e p x )  =  x
263, 23, 7co 6270 . . . . . . . . . 10  class  ( x p e )
2726, 3wceq 1398 . . . . . . . . 9  wff  ( x p e )  =  x
2825, 27wa 367 . . . . . . . 8  wff  ( ( e p x )  =  x  /\  (
x p e )  =  x )
2928, 2, 10wral 2804 . . . . . . 7  wff  A. x  e.  b  ( (
e p x )  =  x  /\  (
x p e )  =  x )
3029, 22, 10wrex 2805 . . . . . 6  wff  E. e  e.  b  A. x  e.  b  ( (
e p x )  =  x  /\  (
x p e )  =  x )
3121, 30wa 367 . . . . 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 1397 . . . . . 6  class  g
34 cplusg 14784 . . . . . 6  class  +g
3533, 34cfv 5570 . . . . 5  class  ( +g  `  g )
3631, 6, 35wsbc 3324 . . . 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 14716 . . . . 5  class  Base
3833, 37cfv 5570 . . . 4  class  ( Base `  g )
3936, 9, 38wsbc 3324 . . 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 2439 . 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 1398 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  16125
  Copyright terms: Public domain W3C validator