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

Definition df-ga 17492
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‘𝑔) / 𝑏{𝑚 ∈ (𝑠𝑚 (𝑏 × 𝑠)) ∣ ∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
Distinct variable group:   𝑔,𝑏,𝑚,𝑠,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ga
StepHypRef Expression
1 cga 17491 . 2 class GrpAct
2 vg . . 3 setvar 𝑔
3 vs . . 3 setvar 𝑠
4 cgrp 17191 . . 3 class Grp
5 cvv 3172 . . 3 class V
6 vb . . . 4 setvar 𝑏
72cv 1473 . . . . 5 class 𝑔
8 cbs 15641 . . . . 5 class Base
97, 8cfv 5790 . . . 4 class (Base‘𝑔)
10 c0g 15869 . . . . . . . . . 10 class 0g
117, 10cfv 5790 . . . . . . . . 9 class (0g𝑔)
12 vx . . . . . . . . . 10 setvar 𝑥
1312cv 1473 . . . . . . . . 9 class 𝑥
14 vm . . . . . . . . . 10 setvar 𝑚
1514cv 1473 . . . . . . . . 9 class 𝑚
1611, 13, 15co 6527 . . . . . . . 8 class ((0g𝑔)𝑚𝑥)
1716, 13wceq 1474 . . . . . . 7 wff ((0g𝑔)𝑚𝑥) = 𝑥
18 vy . . . . . . . . . . . . 13 setvar 𝑦
1918cv 1473 . . . . . . . . . . . 12 class 𝑦
20 vz . . . . . . . . . . . . 13 setvar 𝑧
2120cv 1473 . . . . . . . . . . . 12 class 𝑧
22 cplusg 15714 . . . . . . . . . . . . 13 class +g
237, 22cfv 5790 . . . . . . . . . . . 12 class (+g𝑔)
2419, 21, 23co 6527 . . . . . . . . . . 11 class (𝑦(+g𝑔)𝑧)
2524, 13, 15co 6527 . . . . . . . . . 10 class ((𝑦(+g𝑔)𝑧)𝑚𝑥)
2621, 13, 15co 6527 . . . . . . . . . . 11 class (𝑧𝑚𝑥)
2719, 26, 15co 6527 . . . . . . . . . 10 class (𝑦𝑚(𝑧𝑚𝑥))
2825, 27wceq 1474 . . . . . . . . 9 wff ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))
296cv 1473 . . . . . . . . 9 class 𝑏
3028, 20, 29wral 2895 . . . . . . . 8 wff 𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))
3130, 18, 29wral 2895 . . . . . . 7 wff 𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))
3217, 31wa 382 . . . . . 6 wff (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))
333cv 1473 . . . . . 6 class 𝑠
3432, 12, 33wral 2895 . . . . 5 wff 𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))
3529, 33cxp 5026 . . . . . 6 class (𝑏 × 𝑠)
36 cmap 7721 . . . . . 6 class 𝑚
3733, 35, 36co 6527 . . . . 5 class (𝑠𝑚 (𝑏 × 𝑠))
3834, 14, 37crab 2899 . . . 4 class {𝑚 ∈ (𝑠𝑚 (𝑏 × 𝑠)) ∣ ∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))}
396, 9, 38csb 3498 . . 3 class (Base‘𝑔) / 𝑏{𝑚 ∈ (𝑠𝑚 (𝑏 × 𝑠)) ∣ ∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))}
402, 3, 4, 5, 39cmpt2 6529 . 2 class (𝑔 ∈ Grp, 𝑠 ∈ V ↦ (Base‘𝑔) / 𝑏{𝑚 ∈ (𝑠𝑚 (𝑏 × 𝑠)) ∣ ∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
411, 40wceq 1474 1 wff GrpAct = (𝑔 ∈ Grp, 𝑠 ∈ V ↦ (Base‘𝑔) / 𝑏{𝑚 ∈ (𝑠𝑚 (𝑏 × 𝑠)) ∣ ∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
Colors of variables: wff setvar class
This definition is referenced by:  isga  17493
  Copyright terms: Public domain W3C validator