This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑔 ∈ Grp , 𝑠 ∈ V ↦ ⦋ ( Base ‘ 𝑔 ) / 𝑏 ⦌ { 𝑚 ∈ ( 𝑠 ↑m ( 𝑏 × 𝑠 ) ) ∣ ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cga ⊢ GrpAct
1 vg ⊢ 𝑔
2 cgrp ⊢ Grp
3 vs ⊢ 𝑠
4 cvv ⊢ V
5 cbs ⊢ Base
6 1 cv ⊢ 𝑔
7 6 5 cfv ⊢ ( Base ‘ 𝑔 )
8 vb ⊢ 𝑏
9 vm ⊢ 𝑚
10 3 cv ⊢ 𝑠
11 cmap ⊢ ↑m
12 8 cv ⊢ 𝑏
13 12 10 cxp ⊢ ( 𝑏 × 𝑠 )
14 10 13 11 co ⊢ ( 𝑠 ↑m ( 𝑏 × 𝑠 ) )
15 vx ⊢ 𝑥
16 c0g ⊢ 0g
17 6 16 cfv ⊢ ( 0g ‘ 𝑔 )
18 9 cv ⊢ 𝑚
19 15 cv ⊢ 𝑥
20 17 19 18 co ⊢ ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 )
21 20 19 wceq ⊢ ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥
22 vy ⊢ 𝑦
23 vz ⊢ 𝑧
24 22 cv ⊢ 𝑦
25 cplusg ⊢ +g
26 6 25 cfv ⊢ ( +g ‘ 𝑔 )
27 23 cv ⊢ 𝑧
28 24 27 26 co ⊢ ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 )
29 28 19 18 co ⊢ ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 )
30 27 19 18 co ⊢ ( 𝑧 𝑚 𝑥 )
31 24 30 18 co ⊢ ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) )
32 29 31 wceq ⊢ ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) )
33 32 23 12 wral ⊢ ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) )
34 33 22 12 wral ⊢ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) )
35 21 34 wa ⊢ ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) )
36 35 15 10 wral ⊢ ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) )
37 36 9 14 crab ⊢ { 𝑚 ∈ ( 𝑠 ↑m ( 𝑏 × 𝑠 ) ) ∣ ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) }
38 8 7 37 csb ⊢ ⦋ ( Base ‘ 𝑔 ) / 𝑏 ⦌ { 𝑚 ∈ ( 𝑠 ↑m ( 𝑏 × 𝑠 ) ) ∣ ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) }
39 1 3 2 4 38 cmpo ⊢ ( 𝑔 ∈ Grp , 𝑠 ∈ V ↦ ⦋ ( Base ‘ 𝑔 ) / 𝑏 ⦌ { 𝑚 ∈ ( 𝑠 ↑m ( 𝑏 × 𝑠 ) ) ∣ ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) } )
40 0 39 wceq ⊢ GrpAct = ( 𝑔 ∈ Grp , 𝑠 ∈ V ↦ ⦋ ( Base ‘ 𝑔 ) / 𝑏 ⦌ { 𝑚 ∈ ( 𝑠 ↑m ( 𝑏 × 𝑠 ) ) ∣ ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) } )