Definition df-ga 17723

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

Assertion

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

Distinct variable group:   g, b, m, s, x, y, z

Detailed syntax breakdown of Definition df-ga

Step	Hyp	Ref	Expression
1		cga 17722	. 2 class GrpAct
2		vg	. . 3 setvar g
3		vs	. . 3 setvar s
4		cgrp 17422	. . 3 class Grp
5		cvv 3200	. . 3 class _V
6		vb	. . . 4 setvar b
7	2	cv 1482	. . . . 5 class g
8		cbs 15857	. . . . 5 class Base
9	7, 8	cfv 5888	. . . 4 class ( Base ` g )
10		c0g 16100	. . . . . . . . . 10 class 0g
11	7, 10	cfv 5888	. . . . . . . . 9 class ( 0g ` g )
12		vx	. . . . . . . . . 10 setvar x
13	12	cv 1482	. . . . . . . . 9 class x
14		vm	. . . . . . . . . 10 setvar m
15	14	cv 1482	. . . . . . . . 9 class m
16	11, 13, 15	co 6650	. . . . . . . 8 class ( ( 0g ` g ) m x )
17	16, 13	wceq 1483	. . . . . . 7 wff ( ( 0g ` g ) m x ) = x
18		vy	. . . . . . . . . . . . 13 setvar y
19	18	cv 1482	. . . . . . . . . . . 12 class y
20		vz	. . . . . . . . . . . . 13 setvar z
21	20	cv 1482	. . . . . . . . . . . 12 class z
22		cplusg 15941	. . . . . . . . . . . . 13 class +g
23	7, 22	cfv 5888	. . . . . . . . . . . 12 class ( +g ` g )
24	19, 21, 23	co 6650	. . . . . . . . . . 11 class ( y ( +g ` g ) z )
25	24, 13, 15	co 6650	. . . . . . . . . 10 class ( ( y ( +g ` g ) z ) m x )
26	21, 13, 15	co 6650	. . . . . . . . . . 11 class ( z m x )
27	19, 26, 15	co 6650	. . . . . . . . . 10 class ( y m ( z m x ) )
28	25, 27	wceq 1483	. . . . . . . . 9 wff ( ( y ( +g ` g ) z ) m x ) = ( y m ( z m x ) )
29	6	cv 1482	. . . . . . . . 9 class b
30	28, 20, 29	wral 2912	. . . . . . . 8 wff A. z e. b ( ( y ( +g ` g ) z ) m x ) = ( y m ( z m x ) )
31	30, 18, 29	wral 2912	. . . . . . 7 wff A. y e. b A. z e. b ( ( y ( +g ` g ) z ) m x ) = ( y m ( z m x ) )
32	17, 31	wa 384	. . . . . 6 wff ( ( ( 0g ` g ) m x ) = x /\ A. y e. b A. z e. b ( ( y ( +g ` g ) z ) m x ) = ( y m ( z m x ) ) )
33	3	cv 1482	. . . . . 6 class s
34	32, 12, 33	wral 2912	. . . . 5 wff 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 ) ) )
35	29, 33	cxp 5112	. . . . . 6 class ( b X. s )
36		cmap 7857	. . . . . 6 class ^m
37	33, 35, 36	co 6650	. . . . 5 class ( s ^m ( b X. s ) )
38	34, 14, 37	crab 2916	. . . 4 class { 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	6, 9, 38	csb 3533	. . 3 class [_ ( 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	2, 3, 4, 5, 39	cmpt2 6652	. 2 class ( 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 ) ) ) } )
41	1, 40	wceq 1483	1 wff 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 ) ) ) } )

This definition is referenced by:  isga  17724