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 \in Grp, s \in V ⟼ ⦋ {Base}_{g} / b ⦌ \{m \in (s^{(b \times s)}) \| \forall x \in s (0_{g} m x = x \land \forall y \in b \forall z \in b (y +_{g} z) m x = y m (z m x))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cga	$class GrpAct$
1		vg	$setvar g$
2		cgrp	$class Grp$
3		vs	$setvar s$
4		cvv	$class V$
5		cbs	$class Base$
6	1	cv	$setvar g$
7	6 5	cfv	$class {Base}_{g}$
8		vb	$setvar b$
9		vm	$setvar m$
10	3	cv	$setvar s$
11		cmap	$class ↑_{𝑚}$
12	8	cv	$setvar b$
13	12 10	cxp	$class (b \times s)$
14	10 13 11	co	$class (s^{(b \times s)})$
15		vx	$setvar x$
16		c0g	$class 0_{𝑔}$
17	6 16	cfv	$class 0_{g}$
18	9	cv	$setvar m$
19	15	cv	$setvar x$
20	17 19 18	co	$class (0_{g} m x)$
21	20 19	wceq	$wff 0_{g} m x = x$
22		vy	$setvar y$
23		vz	$setvar z$
24	22	cv	$setvar y$
25		cplusg	$class +_{𝑔}$
26	6 25	cfv	$class +_{g}$
27	23	cv	$setvar z$
28	24 27 26	co	$class (y +_{g} z)$
29	28 19 18	co	$class ((y +_{g} z) m x)$
30	27 19 18	co	$class (z m x)$
31	24 30 18	co	$class (y m (z m x))$
32	29 31	wceq	$wff (y +_{g} z) m x = y m (z m x)$
33	32 23 12	wral	$wff \forall z \in b (y +_{g} z) m x = y m (z m x)$
34	33 22 12	wral	$wff \forall y \in b \forall z \in b (y +_{g} z) m x = y m (z m x)$
35	21 34	wa	$wff (0_{g} m x = x \land \forall y \in b \forall z \in b (y +_{g} z) m x = y m (z m x))$
36	35 15 10	wral	$wff \forall x \in s (0_{g} m x = x \land \forall y \in b \forall z \in b (y +_{g} z) m x = y m (z m x))$
37	36 9 14	crab	$class \{m \in (s^{(b \times s)}) \| \forall x \in s (0_{g} m x = x \land \forall y \in b \forall z \in b (y +_{g} z) m x = y m (z m x))\}$
38	8 7 37	csb	$class ⦋ {Base}_{g} / b ⦌ \{m \in (s^{(b \times s)}) \| \forall x \in s (0_{g} m x = x \land \forall y \in b \forall z \in b (y +_{g} z) m x = y m (z m x))\}$
39	1 3 2 4 38	cmpo	$class (g \in Grp, s \in V ⟼ ⦋ {Base}_{g} / b ⦌ \{m \in (s^{(b \times s)}) \| \forall x \in s (0_{g} m x = x \land \forall y \in b \forall z \in b (y +_{g} z) m x = y m (z m x))\})$
40	0 39	wceq	$wff GrpAct = (g \in Grp, s \in V ⟼ ⦋ {Base}_{g} / b ⦌ \{m \in (s^{(b \times s)}) \| \forall x \in s (0_{g} m x = x \land \forall y \in b \forall z \in b (y +_{g} z) m x = y m (z m x))\})$

Metamath Proof Explorer

Definition df-ga

Detailed syntax breakdown