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

Definition df-ga 15072
 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 15071 . 2
2 vg . . 3
3 vs . . 3
4 cgrp 14690 . . 3
5 cvv 2958 . . 3
6 vb . . . 4
72cv 1652 . . . . 5
8 cbs 13474 . . . . 5
97, 8cfv 5457 . . . 4
10 c0g 13728 . . . . . . . . . 10
117, 10cfv 5457 . . . . . . . . 9
12 vx . . . . . . . . . 10
1312cv 1652 . . . . . . . . 9
14 vm . . . . . . . . . 10
1514cv 1652 . . . . . . . . 9
1611, 13, 15co 6084 . . . . . . . 8
1716, 13wceq 1653 . . . . . . 7
18 vy . . . . . . . . . . . . 13
1918cv 1652 . . . . . . . . . . . 12
20 vz . . . . . . . . . . . . 13
2120cv 1652 . . . . . . . . . . . 12
22 cplusg 13534 . . . . . . . . . . . . 13
237, 22cfv 5457 . . . . . . . . . . . 12
2419, 21, 23co 6084 . . . . . . . . . . 11
2524, 13, 15co 6084 . . . . . . . . . 10
2621, 13, 15co 6084 . . . . . . . . . . 11
2719, 26, 15co 6084 . . . . . . . . . 10
2825, 27wceq 1653 . . . . . . . . 9
296cv 1652 . . . . . . . . 9
3028, 20, 29wral 2707 . . . . . . . 8
3130, 18, 29wral 2707 . . . . . . 7
3217, 31wa 360 . . . . . 6
333cv 1652 . . . . . 6
3432, 12, 33wral 2707 . . . . 5
3529, 33cxp 4879 . . . . . 6
36 cmap 7021 . . . . . 6
3733, 35, 36co 6084 . . . . 5
3834, 14, 37crab 2711 . . . 4
396, 9, 38csb 3253 . . 3
402, 3, 4, 5, 39cmpt2 6086 . 2
411, 40wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  isga  15073
 Copyright terms: Public domain W3C validator