Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ga Structured version   Unicode version

Definition df-ga 15790
 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 to 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
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-ga
StepHypRef Expression
1 cga 15789 . 2
2 vg . . 3
3 vs . . 3
4 cgrp 15395 . . 3
5 cvv 2964 . . 3
6 vb . . . 4
72cv 1363 . . . . 5
8 cbs 14159 . . . . 5
97, 8cfv 5408 . . . 4
10 c0g 14363 . . . . . . . . . 10
117, 10cfv 5408 . . . . . . . . 9
12 vx . . . . . . . . . 10
1312cv 1363 . . . . . . . . 9
14 vm . . . . . . . . . 10
1514cv 1363 . . . . . . . . 9
1611, 13, 15co 6082 . . . . . . . 8
1716, 13wceq 1364 . . . . . . 7
18 vy . . . . . . . . . . . . 13
1918cv 1363 . . . . . . . . . . . 12
20 vz . . . . . . . . . . . . 13
2120cv 1363 . . . . . . . . . . . 12
22 cplusg 14223 . . . . . . . . . . . . 13
237, 22cfv 5408 . . . . . . . . . . . 12
2419, 21, 23co 6082 . . . . . . . . . . 11
2524, 13, 15co 6082 . . . . . . . . . 10
2621, 13, 15co 6082 . . . . . . . . . . 11
2719, 26, 15co 6082 . . . . . . . . . 10
2825, 27wceq 1364 . . . . . . . . 9
296cv 1363 . . . . . . . . 9
3028, 20, 29wral 2707 . . . . . . . 8
3130, 18, 29wral 2707 . . . . . . 7
3217, 31wa 369 . . . . . 6
333cv 1363 . . . . . 6
3432, 12, 33wral 2707 . . . . 5
3529, 33cxp 4827 . . . . . 6
36 cmap 7204 . . . . . 6
3733, 35, 36co 6082 . . . . 5
3834, 14, 37crab 2711 . . . 4
396, 9, 38csb 3278 . . 3
402, 3, 4, 5, 39cmpt2 6084 . 2
411, 40wceq 1364 1
 Colors of variables: wff setvar class This definition is referenced by:  isga  15791
 Copyright terms: Public domain W3C validator