Definition df-ga 18811

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

Assertion

Ref	Expression
df-ga	⊢ GrpAct = (𝑔 ∈ Grp, 𝑠 ∈ V ↦ ⦋(Base‘𝑔) / 𝑏⦌{𝑚 ∈ (𝑠 ↑m (𝑏 × 𝑠)) ∣ ∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})

Distinct variable group:   𝑔,𝑏,𝑚,𝑠,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ga

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

This definition is referenced by:  isga  18812