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

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 ⊕ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ⊕ 𝑥 ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) ) ) )