Metamath Proof Explorer

Theorem conjga

Description: Group conjugation induces a group action. (Contributed by Thierry Arnoux, 18-Nov-2025)

Ref Expression
Hypotheses cntrval2.1 ⊢ 𝐵 = ( Base ‘ 𝑀 )
cntrval2.2 ⊢ + = ( +g ‘ 𝑀 )
cntrval2.3 ⊢ − = ( -g ‘ 𝑀 )
cntrval2.4 ⊢ ⊕ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 + 𝑦 ) − 𝑥 ) )
Assertion conjga ( 𝑀 ∈ Grp → ⊕ ∈ ( 𝑀 GrpAct 𝐵 ) )

Proof

Step Hyp Ref Expression
1 cntrval2.1 ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 cntrval2.2 ⊢ + = ( +g ‘ 𝑀 )
3 cntrval2.3 ⊢ − = ( -g ‘ 𝑀 )
4 cntrval2.4 ⊢ ⊕ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 + 𝑦 ) − 𝑥 ) )
5 id ⊢ ( 𝑀 ∈ Grp → 𝑀 ∈ Grp )
6 1 fvexi ⊢ 𝐵 ∈ V
7 6 a1i ⊢ ( 𝑀 ∈ Grp → 𝐵 ∈ V )
8 5 adantr ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ ( 𝐵 × 𝐵 ) ) → 𝑀 ∈ Grp )
9 xp1st ⊢ ( 𝑧 ∈ ( 𝐵 × 𝐵 ) → ( 1st ‘ 𝑧 ) ∈ 𝐵 )
10 9 adantl ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ ( 𝐵 × 𝐵 ) ) → ( 1st ‘ 𝑧 ) ∈ 𝐵 )
11 xp2nd ⊢ ( 𝑧 ∈ ( 𝐵 × 𝐵 ) → ( 2nd ‘ 𝑧 ) ∈ 𝐵 )
12 11 adantl ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ ( 𝐵 × 𝐵 ) ) → ( 2nd ‘ 𝑧 ) ∈ 𝐵 )
13 1 2 8 10 12 grpcld ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ ( 𝐵 × 𝐵 ) ) → ( ( 1st ‘ 𝑧 ) + ( 2nd ‘ 𝑧 ) ) ∈ 𝐵 )
14 1 3 8 13 10 grpsubcld ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ ( 𝐵 × 𝐵 ) ) → ( ( ( 1st ‘ 𝑧 ) + ( 2nd ‘ 𝑧 ) ) − ( 1st ‘ 𝑧 ) ) ∈ 𝐵 )
15 vex ⊢ 𝑥 ∈ V
16 vex ⊢ 𝑦 ∈ V
17 15 16 op1std ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st ‘ 𝑧 ) = 𝑥 )
18 15 16 op2ndd ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝑧 ) = 𝑦 )
19 17 18 oveq12d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 1st ‘ 𝑧 ) + ( 2nd ‘ 𝑧 ) ) = ( 𝑥 + 𝑦 ) )
20 19 17 oveq12d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 1st ‘ 𝑧 ) + ( 2nd ‘ 𝑧 ) ) − ( 1st ‘ 𝑧 ) ) = ( ( 𝑥 + 𝑦 ) − 𝑥 ) )
21 20 mpompt ⊢ ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( ( ( 1st ‘ 𝑧 ) + ( 2nd ‘ 𝑧 ) ) − ( 1st ‘ 𝑧 ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 + 𝑦 ) − 𝑥 ) )
22 4 21 eqtr4i ⊢ ⊕ = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( ( ( 1st ‘ 𝑧 ) + ( 2nd ‘ 𝑧 ) ) − ( 1st ‘ 𝑧 ) ) )
23 14 22 fmptd ⊢ ( 𝑀 ∈ Grp → ⊕ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
24 4 a1i ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) → ⊕ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 + 𝑦 ) − 𝑥 ) ) )
25 simplr ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 = ( 0g ‘ 𝑀 ) ) ∧ 𝑦 = 𝑧 ) → 𝑥 = ( 0g ‘ 𝑀 ) )
26 simpr ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 = ( 0g ‘ 𝑀 ) ) ∧ 𝑦 = 𝑧 ) → 𝑦 = 𝑧 )
27 25 26 oveq12d ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 = ( 0g ‘ 𝑀 ) ) ∧ 𝑦 = 𝑧 ) → ( 𝑥 + 𝑦 ) = ( ( 0g ‘ 𝑀 ) + 𝑧 ) )
28 27 25 oveq12d ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 = ( 0g ‘ 𝑀 ) ) ∧ 𝑦 = 𝑧 ) → ( ( 𝑥 + 𝑦 ) − 𝑥 ) = ( ( ( 0g ‘ 𝑀 ) + 𝑧 ) − ( 0g ‘ 𝑀 ) ) )
29 5 ad3antrrr ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 = ( 0g ‘ 𝑀 ) ) ∧ 𝑦 = 𝑧 ) → 𝑀 ∈ Grp )
30 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
31 1 30 grpidcl ⊢ ( 𝑀 ∈ Grp → ( 0g ‘ 𝑀 ) ∈ 𝐵 )
32 31 ad3antrrr ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 = ( 0g ‘ 𝑀 ) ) ∧ 𝑦 = 𝑧 ) → ( 0g ‘ 𝑀 ) ∈ 𝐵 )
33 simpllr ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 = ( 0g ‘ 𝑀 ) ) ∧ 𝑦 = 𝑧 ) → 𝑧 ∈ 𝐵 )
34 1 2 29 32 33 grpcld ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 = ( 0g ‘ 𝑀 ) ) ∧ 𝑦 = 𝑧 ) → ( ( 0g ‘ 𝑀 ) + 𝑧 ) ∈ 𝐵 )
35 1 30 3 grpsubid1 ⊢ ( ( 𝑀 ∈ Grp ∧ ( ( 0g ‘ 𝑀 ) + 𝑧 ) ∈ 𝐵 ) → ( ( ( 0g ‘ 𝑀 ) + 𝑧 ) − ( 0g ‘ 𝑀 ) ) = ( ( 0g ‘ 𝑀 ) + 𝑧 ) )
36 29 34 35 syl2anc ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 = ( 0g ‘ 𝑀 ) ) ∧ 𝑦 = 𝑧 ) → ( ( ( 0g ‘ 𝑀 ) + 𝑧 ) − ( 0g ‘ 𝑀 ) ) = ( ( 0g ‘ 𝑀 ) + 𝑧 ) )
37 1 2 30 29 33 grplidd ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 = ( 0g ‘ 𝑀 ) ) ∧ 𝑦 = 𝑧 ) → ( ( 0g ‘ 𝑀 ) + 𝑧 ) = 𝑧 )
38 28 36 37 3eqtrd ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 = ( 0g ‘ 𝑀 ) ) ∧ 𝑦 = 𝑧 ) → ( ( 𝑥 + 𝑦 ) − 𝑥 ) = 𝑧 )
39 38 anasss ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 = ( 0g ‘ 𝑀 ) ∧ 𝑦 = 𝑧 ) ) → ( ( 𝑥 + 𝑦 ) − 𝑥 ) = 𝑧 )
40 31 adantr ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) → ( 0g ‘ 𝑀 ) ∈ 𝐵 )
41 simpr ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
42 24 39 40 41 41 ovmpod ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) → ( ( 0g ‘ 𝑀 ) ⊕ 𝑧 ) = 𝑧 )
43 5 ad3antrrr ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → 𝑀 ∈ Grp )
44 simplr ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
45 simpr ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → 𝑣 ∈ 𝐵 )
46 simpllr ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
47 1 2 43 44 45 46 grpassd ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( ( 𝑢 + 𝑣 ) + 𝑧 ) = ( 𝑢 + ( 𝑣 + 𝑧 ) ) )
48 47 oveq1d ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( ( ( 𝑢 + 𝑣 ) + 𝑧 ) − ( 𝑢 + 𝑣 ) ) = ( ( 𝑢 + ( 𝑣 + 𝑧 ) ) − ( 𝑢 + 𝑣 ) ) )
49 1 2 43 45 46 grpcld ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑣 + 𝑧 ) ∈ 𝐵 )
50 1 2 43 44 49 grpcld ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 + ( 𝑣 + 𝑧 ) ) ∈ 𝐵 )
51 1 2 3 grpsubsub4 ⊢ ( ( 𝑀 ∈ Grp ∧ ( ( 𝑢 + ( 𝑣 + 𝑧 ) ) ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) → ( ( ( 𝑢 + ( 𝑣 + 𝑧 ) ) − 𝑣 ) − 𝑢 ) = ( ( 𝑢 + ( 𝑣 + 𝑧 ) ) − ( 𝑢 + 𝑣 ) ) )
52 43 50 45 44 51 syl13anc ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( ( ( 𝑢 + ( 𝑣 + 𝑧 ) ) − 𝑣 ) − 𝑢 ) = ( ( 𝑢 + ( 𝑣 + 𝑧 ) ) − ( 𝑢 + 𝑣 ) ) )
53 1 2 3 grpaddsubass ⊢ ( ( 𝑀 ∈ Grp ∧ ( 𝑢 ∈ 𝐵 ∧ ( 𝑣 + 𝑧 ) ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( ( 𝑢 + ( 𝑣 + 𝑧 ) ) − 𝑣 ) = ( 𝑢 + ( ( 𝑣 + 𝑧 ) − 𝑣 ) ) )
54 43 44 49 45 53 syl13anc ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( ( 𝑢 + ( 𝑣 + 𝑧 ) ) − 𝑣 ) = ( 𝑢 + ( ( 𝑣 + 𝑧 ) − 𝑣 ) ) )
55 54 oveq1d ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( ( ( 𝑢 + ( 𝑣 + 𝑧 ) ) − 𝑣 ) − 𝑢 ) = ( ( 𝑢 + ( ( 𝑣 + 𝑧 ) − 𝑣 ) ) − 𝑢 ) )
56 48 52 55 3eqtr2d ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( ( ( 𝑢 + 𝑣 ) + 𝑧 ) − ( 𝑢 + 𝑣 ) ) = ( ( 𝑢 + ( ( 𝑣 + 𝑧 ) − 𝑣 ) ) − 𝑢 ) )
57 4 a1i ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ⊕ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 + 𝑦 ) − 𝑥 ) ) )
58 simprl ⊢ ( ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑥 = ( 𝑢 + 𝑣 ) ∧ 𝑦 = 𝑧 ) ) → 𝑥 = ( 𝑢 + 𝑣 ) )
59 simprr ⊢ ( ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑥 = ( 𝑢 + 𝑣 ) ∧ 𝑦 = 𝑧 ) ) → 𝑦 = 𝑧 )
60 58 59 oveq12d ⊢ ( ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑥 = ( 𝑢 + 𝑣 ) ∧ 𝑦 = 𝑧 ) ) → ( 𝑥 + 𝑦 ) = ( ( 𝑢 + 𝑣 ) + 𝑧 ) )
61 60 58 oveq12d ⊢ ( ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑥 = ( 𝑢 + 𝑣 ) ∧ 𝑦 = 𝑧 ) ) → ( ( 𝑥 + 𝑦 ) − 𝑥 ) = ( ( ( 𝑢 + 𝑣 ) + 𝑧 ) − ( 𝑢 + 𝑣 ) ) )
62 1 2 43 44 45 grpcld ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 + 𝑣 ) ∈ 𝐵 )
63 ovexd ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( ( ( 𝑢 + 𝑣 ) + 𝑧 ) − ( 𝑢 + 𝑣 ) ) ∈ V )
64 57 61 62 46 63 ovmpod ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( ( 𝑢 + 𝑣 ) ⊕ 𝑧 ) = ( ( ( 𝑢 + 𝑣 ) + 𝑧 ) − ( 𝑢 + 𝑣 ) ) )
65 simprl ⊢ ( ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑢 ∧ 𝑦 = ( 𝑣 ⊕ 𝑧 ) ) ) → 𝑥 = 𝑢 )
66 simprr ⊢ ( ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑢 ∧ 𝑦 = ( 𝑣 ⊕ 𝑧 ) ) ) → 𝑦 = ( 𝑣 ⊕ 𝑧 ) )
67 simprl ⊢ ( ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑧 ) ) → 𝑥 = 𝑣 )
68 simprr ⊢ ( ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑧 ) ) → 𝑦 = 𝑧 )
69 67 68 oveq12d ⊢ ( ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑧 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑣 + 𝑧 ) )
70 69 67 oveq12d ⊢ ( ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑧 ) ) → ( ( 𝑥 + 𝑦 ) − 𝑥 ) = ( ( 𝑣 + 𝑧 ) − 𝑣 ) )
71 ovexd ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( ( 𝑣 + 𝑧 ) − 𝑣 ) ∈ V )
72 57 70 45 46 71 ovmpod ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑣 ⊕ 𝑧 ) = ( ( 𝑣 + 𝑧 ) − 𝑣 ) )
73 72 adantr ⊢ ( ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑢 ∧ 𝑦 = ( 𝑣 ⊕ 𝑧 ) ) ) → ( 𝑣 ⊕ 𝑧 ) = ( ( 𝑣 + 𝑧 ) − 𝑣 ) )
74 66 73 eqtrd ⊢ ( ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑢 ∧ 𝑦 = ( 𝑣 ⊕ 𝑧 ) ) ) → 𝑦 = ( ( 𝑣 + 𝑧 ) − 𝑣 ) )
75 65 74 oveq12d ⊢ ( ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑢 ∧ 𝑦 = ( 𝑣 ⊕ 𝑧 ) ) ) → ( 𝑥 + 𝑦 ) = ( 𝑢 + ( ( 𝑣 + 𝑧 ) − 𝑣 ) ) )
76 75 65 oveq12d ⊢ ( ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑢 ∧ 𝑦 = ( 𝑣 ⊕ 𝑧 ) ) ) → ( ( 𝑥 + 𝑦 ) − 𝑥 ) = ( ( 𝑢 + ( ( 𝑣 + 𝑧 ) − 𝑣 ) ) − 𝑢 ) )
77 23 ad3antrrr ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ⊕ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
78 77 45 46 fovcdmd ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑣 ⊕ 𝑧 ) ∈ 𝐵 )
79 ovexd ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( ( 𝑢 + ( ( 𝑣 + 𝑧 ) − 𝑣 ) ) − 𝑢 ) ∈ V )
80 57 76 44 78 79 ovmpod ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 ⊕ ( 𝑣 ⊕ 𝑧 ) ) = ( ( 𝑢 + ( ( 𝑣 + 𝑧 ) − 𝑣 ) ) − 𝑢 ) )
81 56 64 80 3eqtr4d ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐵 ) → ( ( 𝑢 + 𝑣 ) ⊕ 𝑧 ) = ( 𝑢 ⊕ ( 𝑣 ⊕ 𝑧 ) ) )
82 81 anasss ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( ( 𝑢 + 𝑣 ) ⊕ 𝑧 ) = ( 𝑢 ⊕ ( 𝑣 ⊕ 𝑧 ) ) )
83 82 ralrimivva ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) → ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 + 𝑣 ) ⊕ 𝑧 ) = ( 𝑢 ⊕ ( 𝑣 ⊕ 𝑧 ) ) )
84 42 83 jca ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 0g ‘ 𝑀 ) ⊕ 𝑧 ) = 𝑧 ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 + 𝑣 ) ⊕ 𝑧 ) = ( 𝑢 ⊕ ( 𝑣 ⊕ 𝑧 ) ) ) )
85 84 ralrimiva ⊢ ( 𝑀 ∈ Grp → ∀ 𝑧 ∈ 𝐵 ( ( ( 0g ‘ 𝑀 ) ⊕ 𝑧 ) = 𝑧 ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 + 𝑣 ) ⊕ 𝑧 ) = ( 𝑢 ⊕ ( 𝑣 ⊕ 𝑧 ) ) ) )
86 1 2 30 isga ⊢ ( ⊕ ∈ ( 𝑀 GrpAct 𝐵 ) ↔ ( ( 𝑀 ∈ Grp ∧ 𝐵 ∈ V ) ∧ ( ⊕ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( ( 0g ‘ 𝑀 ) ⊕ 𝑧 ) = 𝑧 ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( ( 𝑢 + 𝑣 ) ⊕ 𝑧 ) = ( 𝑢 ⊕ ( 𝑣 ⊕ 𝑧 ) ) ) ) ) )
87 5 7 23 85 86 syl22anbrc ⊢ ( 𝑀 ∈ Grp → ⊕ ∈ ( 𝑀 GrpAct 𝐵 ) )