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

Definition df-grpo 20804
Description: Define the class of all group operations. The base set for a group can be determined from its group operation. Based on the definition in Exercise 28 of [Herstein] p. 54. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-grpo  |-  GrpOp  =  {
g  |  E. t
( g : ( t  X.  t ) --> t  /\  A. x  e.  t  A. y  e.  t  A. z  e.  t  ( (
x g y ) g z )  =  ( x g ( y g z ) )  /\  E. u  e.  t  A. x  e.  t  ( (
u g x )  =  x  /\  E. y  e.  t  (
y g x )  =  u ) ) }
Distinct variable group:    t, g, u, x, y, z

Detailed syntax breakdown of Definition df-grpo
StepHypRef Expression
1 cgr 20799 . 2  class  GrpOp
2 vt . . . . . . . 8  set  t
32cv 1618 . . . . . . 7  class  t
43, 3cxp 4645 . . . . . 6  class  ( t  X.  t )
5 vg . . . . . . 7  set  g
65cv 1618 . . . . . 6  class  g
74, 3, 6wf 4655 . . . . 5  wff  g : ( t  X.  t
) --> t
8 vx . . . . . . . . . . . 12  set  x
98cv 1618 . . . . . . . . . . 11  class  x
10 vy . . . . . . . . . . . 12  set  y
1110cv 1618 . . . . . . . . . . 11  class  y
129, 11, 6co 5778 . . . . . . . . . 10  class  ( x g y )
13 vz . . . . . . . . . . 11  set  z
1413cv 1618 . . . . . . . . . 10  class  z
1512, 14, 6co 5778 . . . . . . . . 9  class  ( ( x g y ) g z )
1611, 14, 6co 5778 . . . . . . . . . 10  class  ( y g z )
179, 16, 6co 5778 . . . . . . . . 9  class  ( x g ( y g z ) )
1815, 17wceq 1619 . . . . . . . 8  wff  ( ( x g y ) g z )  =  ( x g ( y g z ) )
1918, 13, 3wral 2516 . . . . . . 7  wff  A. z  e.  t  ( (
x g y ) g z )  =  ( x g ( y g z ) )
2019, 10, 3wral 2516 . . . . . 6  wff  A. y  e.  t  A. z  e.  t  ( (
x g y ) g z )  =  ( x g ( y g z ) )
2120, 8, 3wral 2516 . . . . 5  wff  A. x  e.  t  A. y  e.  t  A. z  e.  t  ( (
x g y ) g z )  =  ( x g ( y g z ) )
22 vu . . . . . . . . . . 11  set  u
2322cv 1618 . . . . . . . . . 10  class  u
2423, 9, 6co 5778 . . . . . . . . 9  class  ( u g x )
2524, 9wceq 1619 . . . . . . . 8  wff  ( u g x )  =  x
2611, 9, 6co 5778 . . . . . . . . . 10  class  ( y g x )
2726, 23wceq 1619 . . . . . . . . 9  wff  ( y g x )  =  u
2827, 10, 3wrex 2517 . . . . . . . 8  wff  E. y  e.  t  ( y
g x )  =  u
2925, 28wa 360 . . . . . . 7  wff  ( ( u g x )  =  x  /\  E. y  e.  t  (
y g x )  =  u )
3029, 8, 3wral 2516 . . . . . 6  wff  A. x  e.  t  ( (
u g x )  =  x  /\  E. y  e.  t  (
y g x )  =  u )
3130, 22, 3wrex 2517 . . . . 5  wff  E. u  e.  t  A. x  e.  t  ( (
u g x )  =  x  /\  E. y  e.  t  (
y g x )  =  u )
327, 21, 31w3a 939 . . . 4  wff  ( g : ( t  X.  t ) --> t  /\  A. x  e.  t  A. y  e.  t  A. z  e.  t  (
( x g y ) g z )  =  ( x g ( y g z ) )  /\  E. u  e.  t  A. x  e.  t  (
( u g x )  =  x  /\  E. y  e.  t  ( y g x )  =  u ) )
3332, 2wex 1537 . . 3  wff  E. t
( g : ( t  X.  t ) --> t  /\  A. x  e.  t  A. y  e.  t  A. z  e.  t  ( (
x g y ) g z )  =  ( x g ( y g z ) )  /\  E. u  e.  t  A. x  e.  t  ( (
u g x )  =  x  /\  E. y  e.  t  (
y g x )  =  u ) )
3433, 5cab 2242 . 2  class  { g  |  E. t ( g : ( t  X.  t ) --> t  /\  A. x  e.  t  A. y  e.  t  A. z  e.  t  ( ( x g y ) g z )  =  ( x g ( y g z ) )  /\  E. u  e.  t  A. x  e.  t  ( ( u g x )  =  x  /\  E. y  e.  t  ( y
g x )  =  u ) ) }
351, 34wceq 1619 1  wff  GrpOp  =  {
g  |  E. t
( g : ( t  X.  t ) --> t  /\  A. x  e.  t  A. y  e.  t  A. z  e.  t  ( (
x g y ) g z )  =  ( x g ( y g z ) )  /\  E. u  e.  t  A. x  e.  t  ( (
u g x )  =  x  /\  E. y  e.  t  (
y g x )  =  u ) ) }
Colors of variables: wff set class
This definition is referenced by:  isgrpo  20809
  Copyright terms: Public domain W3C validator