Metamath Proof Explorer

Theorem isga

Description: The predicate "is a (left) group action". The group G is said to act on the base set Y of the action, which is not assumed to have any special properties. There is a related notion of right group action, but as the Wikipedia article explains, it is not mathematically interesting. The way actions are usually thought of is that each element g of G is a permutation of the elements of Y (see gapm ). Since group theory was classically about symmetry groups, it is therefore likely that the notion of group action was useful even in early group theory. (Contributed by Jeff Hankins, 10-Aug-2009) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses isga.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
isga.2 ⊢ + = ( +g ‘ 𝐺 )
isga.3 ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion isga ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ V ) ∧ ( ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑌 ( ( 0 ⊕ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ⊕ 𝑥 ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isga.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 isga.2 ⊢ + = ( +g ‘ 𝐺 )
3 isga.3 ⊢ 0 = ( 0g ‘ 𝐺 )
4 df-ga ⊢ GrpAct = ( 𝑔 ∈ Grp , 𝑠 ∈ V ↦ ⦋ ( Base ‘ 𝑔 ) / 𝑏 ⦌ { 𝑚 ∈ ( 𝑠 ↑m ( 𝑏 × 𝑠 ) ) ∣ ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) } )
5 4 elmpocl ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ( 𝐺 ∈ Grp ∧ 𝑌 ∈ V ) )
6 fvexd ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) → ( Base ‘ 𝑔 ) ∈ V )
7 simplr ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → 𝑠 = 𝑌 )
8 id ⊢ ( 𝑏 = ( Base ‘ 𝑔 ) → 𝑏 = ( Base ‘ 𝑔 ) )
9 simpl ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) → 𝑔 = 𝐺 )
10 9 fveq2d ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
11 10 1 eqtr4di ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) → ( Base ‘ 𝑔 ) = 𝑋 )
12 8 11 sylan9eqr ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → 𝑏 = 𝑋 )
13 12 7 xpeq12d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → ( 𝑏 × 𝑠 ) = ( 𝑋 × 𝑌 ) )
14 7 13 oveq12d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → ( 𝑠 ↑m ( 𝑏 × 𝑠 ) ) = ( 𝑌 ↑m ( 𝑋 × 𝑌 ) ) )
15 simpll ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → 𝑔 = 𝐺 )
16 15 fveq2d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → ( 0g ‘ 𝑔 ) = ( 0g ‘ 𝐺 ) )
17 16 3 eqtr4di ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → ( 0g ‘ 𝑔 ) = 0 )
18 17 oveq1d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = ( 0 𝑚 𝑥 ) )
19 18 eqeq1d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ↔ ( 0 𝑚 𝑥 ) = 𝑥 ) )
20 15 fveq2d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → ( +g ‘ 𝑔 ) = ( +g ‘ 𝐺 ) )
21 20 2 eqtr4di ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → ( +g ‘ 𝑔 ) = + )
22 21 oveqd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) = ( 𝑦 + 𝑧 ) )
23 22 oveq1d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) )
24 23 eqeq1d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → ( ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ↔ ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) )
25 12 24 raleqbidv ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → ( ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) )
26 12 25 raleqbidv ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → ( ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) )
27 19 26 anbi12d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → ( ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) ↔ ( ( 0 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) ) )
28 7 27 raleqbidv ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → ( ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝑌 ( ( 0 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) ) )
29 14 28 rabeqbidv ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) ∧ 𝑏 = ( Base ‘ 𝑔 ) ) → { 𝑚 ∈ ( 𝑠 ↑m ( 𝑏 × 𝑠 ) ) ∣ ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) } = { 𝑚 ∈ ( 𝑌 ↑m ( 𝑋 × 𝑌 ) ) ∣ ∀ 𝑥 ∈ 𝑌 ( ( 0 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) } )
30 6 29 csbied ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑌 ) → ⦋ ( Base ‘ 𝑔 ) / 𝑏 ⦌ { 𝑚 ∈ ( 𝑠 ↑m ( 𝑏 × 𝑠 ) ) ∣ ∀ 𝑥 ∈ 𝑠 ( ( ( 0g ‘ 𝑔 ) 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑦 ( +g ‘ 𝑔 ) 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) } = { 𝑚 ∈ ( 𝑌 ↑m ( 𝑋 × 𝑌 ) ) ∣ ∀ 𝑥 ∈ 𝑌 ( ( 0 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) } )
31 ovex ⊢ ( 𝑌 ↑m ( 𝑋 × 𝑌 ) ) ∈ V
32 31 rabex ⊢ { 𝑚 ∈ ( 𝑌 ↑m ( 𝑋 × 𝑌 ) ) ∣ ∀ 𝑥 ∈ 𝑌 ( ( 0 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) } ∈ V
33 30 4 32 ovmpoa ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ V ) → ( 𝐺 GrpAct 𝑌 ) = { 𝑚 ∈ ( 𝑌 ↑m ( 𝑋 × 𝑌 ) ) ∣ ∀ 𝑥 ∈ 𝑌 ( ( 0 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) } )
34 33 eleq2d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ V ) → ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ↔ ⊕ ∈ { 𝑚 ∈ ( 𝑌 ↑m ( 𝑋 × 𝑌 ) ) ∣ ∀ 𝑥 ∈ 𝑌 ( ( 0 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) } ) )
35 oveq ⊢ ( 𝑚 = ⊕ → ( 0 𝑚 𝑥 ) = ( 0 ⊕ 𝑥 ) )
36 35 eqeq1d ⊢ ( 𝑚 = ⊕ → ( ( 0 𝑚 𝑥 ) = 𝑥 ↔ ( 0 ⊕ 𝑥 ) = 𝑥 ) )
37 oveq ⊢ ( 𝑚 = ⊕ → ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( ( 𝑦 + 𝑧 ) ⊕ 𝑥 ) )
38 oveq ⊢ ( 𝑚 = ⊕ → ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) = ( 𝑦 ⊕ ( 𝑧 𝑚 𝑥 ) ) )
39 oveq ⊢ ( 𝑚 = ⊕ → ( 𝑧 𝑚 𝑥 ) = ( 𝑧 ⊕ 𝑥 ) )
40 39 oveq2d ⊢ ( 𝑚 = ⊕ → ( 𝑦 ⊕ ( 𝑧 𝑚 𝑥 ) ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) )
41 38 40 eqtrd ⊢ ( 𝑚 = ⊕ → ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) )
42 37 41 eqeq12d ⊢ ( 𝑚 = ⊕ → ( ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ↔ ( ( 𝑦 + 𝑧 ) ⊕ 𝑥 ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) )
43 42 2ralbidv ⊢ ( 𝑚 = ⊕ → ( ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ⊕ 𝑥 ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) )
44 36 43 anbi12d ⊢ ( 𝑚 = ⊕ → ( ( ( 0 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) ↔ ( ( 0 ⊕ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ⊕ 𝑥 ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) ) )
45 44 ralbidv ⊢ ( 𝑚 = ⊕ → ( ∀ 𝑥 ∈ 𝑌 ( ( 0 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝑌 ( ( 0 ⊕ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ⊕ 𝑥 ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) ) )
46 45 elrab ⊢ ( ⊕ ∈ { 𝑚 ∈ ( 𝑌 ↑m ( 𝑋 × 𝑌 ) ) ∣ ∀ 𝑥 ∈ 𝑌 ( ( 0 𝑚 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) 𝑚 𝑥 ) = ( 𝑦 𝑚 ( 𝑧 𝑚 𝑥 ) ) ) } ↔ ( ⊕ ∈ ( 𝑌 ↑m ( 𝑋 × 𝑌 ) ) ∧ ∀ 𝑥 ∈ 𝑌 ( ( 0 ⊕ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ⊕ 𝑥 ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) ) )
47 34 46 bitrdi ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ V ) → ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ↔ ( ⊕ ∈ ( 𝑌 ↑m ( 𝑋 × 𝑌 ) ) ∧ ∀ 𝑥 ∈ 𝑌 ( ( 0 ⊕ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ⊕ 𝑥 ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) ) ) )
48 simpr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ V ) → 𝑌 ∈ V )
49 1 fvexi ⊢ 𝑋 ∈ V
50 xpexg ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 × 𝑌 ) ∈ V )
51 49 48 50 sylancr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ V ) → ( 𝑋 × 𝑌 ) ∈ V )
52 48 51 elmapd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ V ) → ( ⊕ ∈ ( 𝑌 ↑m ( 𝑋 × 𝑌 ) ) ↔ ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 ) )
53 52 anbi1d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ V ) → ( ( ⊕ ∈ ( 𝑌 ↑m ( 𝑋 × 𝑌 ) ) ∧ ∀ 𝑥 ∈ 𝑌 ( ( 0 ⊕ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ⊕ 𝑥 ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) ) ↔ ( ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑌 ( ( 0 ⊕ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ⊕ 𝑥 ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) ) ) )
54 47 53 bitrd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ V ) → ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ↔ ( ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑌 ( ( 0 ⊕ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ⊕ 𝑥 ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) ) ) )
55 5 54 biadanii ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ V ) ∧ ( ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑌 ( ( 0 ⊕ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ⊕ 𝑥 ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) ) ) )