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 ∈ Grp , s ∈ V ⟼ ⦋ Base g / b⦌ m ∈ s b × s | ∀ x ∈ s 0 g m x = x ∧ ∀ y ∈ b ∀ z ∈ 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 × s
14 10 13 11 co class s b × 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 ∀ z ∈ b y + g z m x = y m z m x
34 33 22 12 wral wff ∀ y ∈ b ∀ z ∈ b y + g z m x = y m z m x
35 21 34 wa wff 0 g m x = x ∧ ∀ y ∈ b ∀ z ∈ b y + g z m x = y m z m x
36 35 15 10 wral wff ∀ x ∈ s 0 g m x = x ∧ ∀ y ∈ b ∀ z ∈ b y + g z m x = y m z m x
37 36 9 14 crab class m ∈ s b × s | ∀ x ∈ s 0 g m x = x ∧ ∀ y ∈ b ∀ z ∈ b y + g z m x = y m z m x
38 8 7 37 csb class ⦋ Base g / b⦌ m ∈ s b × s | ∀ x ∈ s 0 g m x = x ∧ ∀ y ∈ b ∀ z ∈ b y + g z m x = y m z m x
39 1 3 2 4 38 cmpo class g ∈ Grp , s ∈ V ⟼ ⦋ Base g / b⦌ m ∈ s b × s | ∀ x ∈ s 0 g m x = x ∧ ∀ y ∈ b ∀ z ∈ b y + g z m x = y m z m x
40 0 39 wceq wff GrpAct = g ∈ Grp , s ∈ V ⟼ ⦋ Base g / b⦌ m ∈ s b × s | ∀ x ∈ s 0 g m x = x ∧ ∀ y ∈ b ∀ z ∈ b y + g z m x = y m z m x