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 = ( 𝑔 ∈ Grp , 𝑠 ∈ V ↦ ⦋ ( Base ‘ 𝑔 ) / 𝑏 ⦌ { 𝑚 ∈ ( 𝑠 ↑m ( 𝑏 × 𝑠 ) ) ∣ ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cga	⊢ GrpAct
1		vg	⊢ 𝑔
2		cgrp	⊢ Grp
3		vs	⊢ 𝑠
4		cvv	⊢ V
5		cbs	⊢ Base
6	1	cv	⊢ 𝑔
7	6 5	cfv	⊢ ( Base ‘ 𝑔 )
8		vb	⊢ 𝑏
9		vm	⊢ 𝑚
10	3	cv	⊢ 𝑠
11		cmap	⊢ ↑m
12	8	cv	⊢ 𝑏
13	12 10	cxp	⊢ ( 𝑏 × 𝑠 )
14	10 13 11	co	⊢ ( 𝑠 ↑m ( 𝑏 × 𝑠 ) )
15		vx	⊢ 𝑥
16		c0g	⊢ 0g
17	6 16	cfv	⊢ ( 0g ‘ 𝑔 )
18	9	cv	⊢ 𝑚
19	15	cv	⊢ 𝑥
20	17 19 18	co	⊢ ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 )
21	20 19	wceq	⊢ ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥
22		vy	⊢ 𝑦
23		vz	⊢ 𝑧
24	22	cv	⊢ 𝑦
25		cplusg	⊢ +g
26	6 25	cfv	⊢ ( +g ‘ 𝑔 )
27	23	cv	⊢ 𝑧
28	24 27 26	co	⊢ ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 )
29	28 19 18	co	⊢ ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 )
30	27 19 18	co	⊢ ( 𝑧 𝑚 𝑥 )
31	24 30 18	co	⊢ ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) )
32	29 31	wceq	⊢ ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) )
33	32 23 12	wral	⊢ ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) )
34	33 22 12	wral	⊢ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) )
35	21 34	wa	⊢ ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) )
36	35 15 10	wral	⊢ ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) )
37	36 9 14	crab	⊢ { 𝑚 ∈ ( 𝑠 ↑m ( 𝑏 × 𝑠 ) ) ∣ ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) }
38	8 7 37	csb	⊢ ⦋ ( Base ‘ 𝑔 ) / 𝑏 ⦌ { 𝑚 ∈ ( 𝑠 ↑m ( 𝑏 × 𝑠 ) ) ∣ ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) }
39	1 3 2 4 38	cmpo	⊢ ( 𝑔 ∈ Grp , 𝑠 ∈ V ↦ ⦋ ( Base ‘ 𝑔 ) / 𝑏 ⦌ { 𝑚 ∈ ( 𝑠 ↑m ( 𝑏 × 𝑠 ) ) ∣ ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) } )
40	0 39	wceq	⊢ GrpAct = ( 𝑔 ∈ Grp , 𝑠 ∈ V ↦ ⦋ ( Base ‘ 𝑔 ) / 𝑏 ⦌ { 𝑚 ∈ ( 𝑠 ↑m ( 𝑏 × 𝑠 ) ) ∣ ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) } )