Metamath Proof Explorer

Definition df-ga

Description: Define the class of all group actions. A group G acts on a set S if a permutation on S is associated with every element of G in such a way that the identity permutation on S is associated with the neutral element of G , and the composition of the permutations associated with two elements of G is identical with the permutation associated with the composition of these two elements (in the same order) in the group G . (Contributed by Jeff Hankins, 10-Aug-2009)

Ref Expression
Assertion df-ga 
|- GrpAct = ( g e. Grp , s e. _V |-> [_ ( Base ` g ) / b ]_ { m e. ( s ^m ( b X. s ) ) | A. x e. s ( ( ( 0g ` g ) m x ) = x /\ A. y e. b A. z e. b ( ( y ( +g ` g ) z ) m x ) = ( y m ( z m x ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cga 
 |-  GrpAct
1 vg 
 |-  g
2 cgrp 
 |-  Grp
3 vs 
 |-  s
4 cvv 
 |-  _V
5 cbs 
 |-  Base
6 1 cv 
 |-  g
7 6 5 cfv 
 |-  ( Base ` g )
8 vb 
 |-  b
9 vm 
 |-  m
10 3 cv 
 |-  s
11 cmap 
 |-  ^m
12 8 cv 
 |-  b
13 12 10 cxp 
 |-  ( b X. s )
14 10 13 11 co 
 |-  ( s ^m ( b X. s ) )
15 vx 
 |-  x
16 c0g 
 |-  0g
17 6 16 cfv 
 |-  ( 0g ` g )
18 9 cv 
 |-  m
19 15 cv 
 |-  x
20 17 19 18 co 
 |-  ( ( 0g ` g ) m x )
21 20 19 wceq 
 |-  ( ( 0g ` g ) m x ) = x
22 vy 
 |-  y
23 vz 
 |-  z
24 22 cv 
 |-  y
25 cplusg 
 |-  +g
26 6 25 cfv 
 |-  ( +g ` g )
27 23 cv 
 |-  z
28 24 27 26 co 
 |-  ( y ( +g ` g ) z )
29 28 19 18 co 
 |-  ( ( y ( +g ` g ) z ) m x )
30 27 19 18 co 
 |-  ( z m x )
31 24 30 18 co 
 |-  ( y m ( z m x ) )
32 29 31 wceq 
 |-  ( ( y ( +g ` g ) z ) m x ) = ( y m ( z m x ) )
33 32 23 12 wral 
 |-  A. z e. b ( ( y ( +g ` g ) z ) m x ) = ( y m ( z m x ) )
34 33 22 12 wral 
 |-  A. y e. b A. z e. b ( ( y ( +g ` g ) z ) m x ) = ( y m ( z m x ) )
35 21 34 wa 
 |-  ( ( ( 0g ` g ) m x ) = x /\ A. y e. b A. z e. b ( ( y ( +g ` g ) z ) m x ) = ( y m ( z m x ) ) )
36 35 15 10 wral 
 |-  A. x e. s ( ( ( 0g ` g ) m x ) = x /\ A. y e. b A. z e. b ( ( y ( +g ` g ) z ) m x ) = ( y m ( z m x ) ) )
37 36 9 14 crab 
 |-  { m e. ( s ^m ( b X. s ) ) | A. x e. s ( ( ( 0g ` g ) m x ) = x /\ A. y e. b A. z e. b ( ( y ( +g ` g ) z ) m x ) = ( y m ( z m x ) ) ) }
38 8 7 37 csb 
 |-  [_ ( Base ` g ) / b ]_ { m e. ( s ^m ( b X. s ) ) | A. x e. s ( ( ( 0g ` g ) m x ) = x /\ A. y e. b A. z e. b ( ( y ( +g ` g ) z ) m x ) = ( y m ( z m x ) ) ) }
39 1 3 2 4 38 cmpo 
 |-  ( g e. Grp , s e. _V |-> [_ ( Base ` g ) / b ]_ { m e. ( s ^m ( b X. s ) ) | A. x e. s ( ( ( 0g ` g ) m x ) = x /\ A. y e. b A. z e. b ( ( y ( +g ` g ) z ) m x ) = ( y m ( z m x ) ) ) } )
40 0 39 wceq 
 |-  GrpAct = ( g e. Grp , s e. _V |-> [_ ( Base ` g ) / b ]_ { m e. ( s ^m ( b X. s ) ) | A. x e. s ( ( ( 0g ` g ) m x ) = x /\ A. y e. b A. z e. b ( ( y ( +g ` g ) z ) m x ) = ( y m ( z m x ) ) ) } )