Metamath Proof Explorer

Definition df-grpo

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.)

Ref Expression
Assertion 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 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgr 
 |-  GrpOp
1 vg 
 |-  g
2 vt 
 |-  t
3 1 cv 
 |-  g
4 2 cv 
 |-  t
5 4 4 cxp 
 |-  ( t X. t )
6 5 4 3 wf 
 |-  g : ( t X. t ) --> t
7 vx 
 |-  x
8 vy 
 |-  y
9 vz 
 |-  z
10 7 cv 
 |-  x
11 8 cv 
 |-  y
12 10 11 3 co 
 |-  ( x g y )
13 9 cv 
 |-  z
14 12 13 3 co 
 |-  ( ( x g y ) g z )
15 11 13 3 co 
 |-  ( y g z )
16 10 15 3 co 
 |-  ( x g ( y g z ) )
17 14 16 wceq 
 |-  ( ( x g y ) g z ) = ( x g ( y g z ) )
18 17 9 4 wral 
 |-  A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) )
19 18 8 4 wral 
 |-  A. y e. t A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) )
20 19 7 4 wral 
 |-  A. x e. t A. y e. t A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) )
21 vu 
 |-  u
22 21 cv 
 |-  u
23 22 10 3 co 
 |-  ( u g x )
24 23 10 wceq 
 |-  ( u g x ) = x
25 11 10 3 co 
 |-  ( y g x )
26 25 22 wceq 
 |-  ( y g x ) = u
27 26 8 4 wrex 
 |-  E. y e. t ( y g x ) = u
28 24 27 wa 
 |-  ( ( u g x ) = x /\ E. y e. t ( y g x ) = u )
29 28 7 4 wral 
 |-  A. x e. t ( ( u g x ) = x /\ E. y e. t ( y g x ) = u )
30 29 21 4 wrex 
 |-  E. u e. t A. x e. t ( ( u g x ) = x /\ E. y e. t ( y g x ) = u )
31 6 20 30 w3a 
 |-  ( 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 ) )
32 31 2 wex 
 |-  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 ) )
33 32 1 cab 
 |-  { 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 ) ) }
34 0 33 wceq 
 |-  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 ) ) }