Metamath Proof Explorer


Theorem mulgass

Description: Product of group multiples, generalized to ZZ . (Contributed by Mario Carneiro, 13-Dec-2014)

Ref Expression
Hypotheses mulgass.b 𝐵 = ( Base ‘ 𝐺 )
mulgass.t · = ( .g𝐺 )
Assertion mulgass ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 mulgass.b 𝐵 = ( Base ‘ 𝐺 )
2 mulgass.t · = ( .g𝐺 )
3 simpr1 ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → 𝑀 ∈ ℤ )
4 elznn0 ( 𝑀 ∈ ℤ ↔ ( 𝑀 ∈ ℝ ∧ ( 𝑀 ∈ ℕ0 ∨ - 𝑀 ∈ ℕ0 ) ) )
5 4 simprbi ( 𝑀 ∈ ℤ → ( 𝑀 ∈ ℕ0 ∨ - 𝑀 ∈ ℕ0 ) )
6 3 5 syl ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( 𝑀 ∈ ℕ0 ∨ - 𝑀 ∈ ℕ0 ) )
7 simpr2 ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → 𝑁 ∈ ℤ )
8 elznn0 ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) ) )
9 8 simprbi ( 𝑁 ∈ ℤ → ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) )
10 7 9 syl ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) )
11 grpmnd ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
12 11 ad2antrr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → 𝐺 ∈ Mnd )
13 simprl ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → 𝑀 ∈ ℕ0 )
14 simprr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℕ0 )
15 simplr3 ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → 𝑋𝐵 )
16 1 2 mulgnn0ass ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0𝑋𝐵 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
17 12 13 14 15 16 syl13anc ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
18 17 ex ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
19 3 zcnd ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → 𝑀 ∈ ℂ )
20 7 zcnd ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → 𝑁 ∈ ℂ )
21 19 20 mulneg1d ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( - 𝑀 · 𝑁 ) = - ( 𝑀 · 𝑁 ) )
22 21 adantr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( - 𝑀 · 𝑁 ) = - ( 𝑀 · 𝑁 ) )
23 22 oveq1d ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( - 𝑀 · 𝑁 ) · 𝑋 ) = ( - ( 𝑀 · 𝑁 ) · 𝑋 ) )
24 11 ad2antrr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → 𝐺 ∈ Mnd )
25 simprl ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → - 𝑀 ∈ ℕ0 )
26 simprr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℕ0 )
27 simpr3 ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → 𝑋𝐵 )
28 27 adantr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → 𝑋𝐵 )
29 1 2 mulgnn0ass ( ( 𝐺 ∈ Mnd ∧ ( - 𝑀 ∈ ℕ0𝑁 ∈ ℕ0𝑋𝐵 ) ) → ( ( - 𝑀 · 𝑁 ) · 𝑋 ) = ( - 𝑀 · ( 𝑁 · 𝑋 ) ) )
30 24 25 26 28 29 syl13anc ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( - 𝑀 · 𝑁 ) · 𝑋 ) = ( - 𝑀 · ( 𝑁 · 𝑋 ) ) )
31 23 30 eqtr3d ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( - ( 𝑀 · 𝑁 ) · 𝑋 ) = ( - 𝑀 · ( 𝑁 · 𝑋 ) ) )
32 fveq2 ( ( - ( 𝑀 · 𝑁 ) · 𝑋 ) = ( - 𝑀 · ( 𝑁 · 𝑋 ) ) → ( ( invg𝐺 ) ‘ ( - ( 𝑀 · 𝑁 ) · 𝑋 ) ) = ( ( invg𝐺 ) ‘ ( - 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
33 simpl ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → 𝐺 ∈ Grp )
34 3 7 zmulcld ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
35 eqid ( invg𝐺 ) = ( invg𝐺 )
36 1 2 35 mulgneg ( ( 𝐺 ∈ Grp ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ∧ 𝑋𝐵 ) → ( - ( 𝑀 · 𝑁 ) · 𝑋 ) = ( ( invg𝐺 ) ‘ ( ( 𝑀 · 𝑁 ) · 𝑋 ) ) )
37 33 34 27 36 syl3anc ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( - ( 𝑀 · 𝑁 ) · 𝑋 ) = ( ( invg𝐺 ) ‘ ( ( 𝑀 · 𝑁 ) · 𝑋 ) ) )
38 37 fveq2d ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( invg𝐺 ) ‘ ( - ( 𝑀 · 𝑁 ) · 𝑋 ) ) = ( ( invg𝐺 ) ‘ ( ( invg𝐺 ) ‘ ( ( 𝑀 · 𝑁 ) · 𝑋 ) ) ) )
39 1 2 mulgcl ( ( 𝐺 ∈ Grp ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ∧ 𝑋𝐵 ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) ∈ 𝐵 )
40 33 34 27 39 syl3anc ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) ∈ 𝐵 )
41 1 35 grpinvinv ( ( 𝐺 ∈ Grp ∧ ( ( 𝑀 · 𝑁 ) · 𝑋 ) ∈ 𝐵 ) → ( ( invg𝐺 ) ‘ ( ( invg𝐺 ) ‘ ( ( 𝑀 · 𝑁 ) · 𝑋 ) ) ) = ( ( 𝑀 · 𝑁 ) · 𝑋 ) )
42 40 41 syldan ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( invg𝐺 ) ‘ ( ( invg𝐺 ) ‘ ( ( 𝑀 · 𝑁 ) · 𝑋 ) ) ) = ( ( 𝑀 · 𝑁 ) · 𝑋 ) )
43 38 42 eqtrd ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( invg𝐺 ) ‘ ( - ( 𝑀 · 𝑁 ) · 𝑋 ) ) = ( ( 𝑀 · 𝑁 ) · 𝑋 ) )
44 1 2 mulgcl ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
45 33 7 27 44 syl3anc ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
46 1 2 35 mulgneg ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( - 𝑀 · ( 𝑁 · 𝑋 ) ) = ( ( invg𝐺 ) ‘ ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
47 33 3 45 46 syl3anc ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( - 𝑀 · ( 𝑁 · 𝑋 ) ) = ( ( invg𝐺 ) ‘ ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
48 47 fveq2d ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( invg𝐺 ) ‘ ( - 𝑀 · ( 𝑁 · 𝑋 ) ) ) = ( ( invg𝐺 ) ‘ ( ( invg𝐺 ) ‘ ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) ) )
49 1 2 mulgcl ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( 𝑀 · ( 𝑁 · 𝑋 ) ) ∈ 𝐵 )
50 33 3 45 49 syl3anc ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( 𝑀 · ( 𝑁 · 𝑋 ) ) ∈ 𝐵 )
51 1 35 grpinvinv ( ( 𝐺 ∈ Grp ∧ ( 𝑀 · ( 𝑁 · 𝑋 ) ) ∈ 𝐵 ) → ( ( invg𝐺 ) ‘ ( ( invg𝐺 ) ‘ ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
52 50 51 syldan ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( invg𝐺 ) ‘ ( ( invg𝐺 ) ‘ ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
53 48 52 eqtrd ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( invg𝐺 ) ‘ ( - 𝑀 · ( 𝑁 · 𝑋 ) ) ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
54 43 53 eqeq12d ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( ( invg𝐺 ) ‘ ( - ( 𝑀 · 𝑁 ) · 𝑋 ) ) = ( ( invg𝐺 ) ‘ ( - 𝑀 · ( 𝑁 · 𝑋 ) ) ) ↔ ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
55 32 54 syl5ib ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( - ( 𝑀 · 𝑁 ) · 𝑋 ) = ( - 𝑀 · ( 𝑁 · 𝑋 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
56 55 imp ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - ( 𝑀 · 𝑁 ) · 𝑋 ) = ( - 𝑀 · ( 𝑁 · 𝑋 ) ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
57 31 56 syldan ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
58 57 ex ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( - 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
59 11 ad2antrr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → 𝐺 ∈ Mnd )
60 simprl ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → 𝑀 ∈ ℕ0 )
61 simprr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → - 𝑁 ∈ ℕ0 )
62 27 adantr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → 𝑋𝐵 )
63 1 2 mulgnn0ass ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0𝑋𝐵 ) ) → ( ( 𝑀 · - 𝑁 ) · 𝑋 ) = ( 𝑀 · ( - 𝑁 · 𝑋 ) ) )
64 59 60 61 62 63 syl13anc ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 · - 𝑁 ) · 𝑋 ) = ( 𝑀 · ( - 𝑁 · 𝑋 ) ) )
65 19 20 mulneg2d ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( 𝑀 · - 𝑁 ) = - ( 𝑀 · 𝑁 ) )
66 65 adantr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( 𝑀 · - 𝑁 ) = - ( 𝑀 · 𝑁 ) )
67 66 oveq1d ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 · - 𝑁 ) · 𝑋 ) = ( - ( 𝑀 · 𝑁 ) · 𝑋 ) )
68 1 2 35 mulgneg ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) → ( - 𝑁 · 𝑋 ) = ( ( invg𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) )
69 33 7 27 68 syl3anc ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( - 𝑁 · 𝑋 ) = ( ( invg𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) )
70 69 oveq2d ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( 𝑀 · ( - 𝑁 · 𝑋 ) ) = ( 𝑀 · ( ( invg𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) ) )
71 1 2 35 mulgneg2 ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( - 𝑀 · ( 𝑁 · 𝑋 ) ) = ( 𝑀 · ( ( invg𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) ) )
72 33 3 45 71 syl3anc ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( - 𝑀 · ( 𝑁 · 𝑋 ) ) = ( 𝑀 · ( ( invg𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) ) )
73 70 72 eqtr4d ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( 𝑀 · ( - 𝑁 · 𝑋 ) ) = ( - 𝑀 · ( 𝑁 · 𝑋 ) ) )
74 73 adantr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( 𝑀 · ( - 𝑁 · 𝑋 ) ) = ( - 𝑀 · ( 𝑁 · 𝑋 ) ) )
75 64 67 74 3eqtr3d ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( - ( 𝑀 · 𝑁 ) · 𝑋 ) = ( - 𝑀 · ( 𝑁 · 𝑋 ) ) )
76 75 56 syldan ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
77 76 ex ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
78 11 ad2antrr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → 𝐺 ∈ Mnd )
79 simprl ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → - 𝑀 ∈ ℕ0 )
80 simprr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → - 𝑁 ∈ ℕ0 )
81 27 adantr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → 𝑋𝐵 )
82 1 2 mulgnn0ass ( ( 𝐺 ∈ Mnd ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0𝑋𝐵 ) ) → ( ( - 𝑀 · - 𝑁 ) · 𝑋 ) = ( - 𝑀 · ( - 𝑁 · 𝑋 ) ) )
83 78 79 80 81 82 syl13anc ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( - 𝑀 · - 𝑁 ) · 𝑋 ) = ( - 𝑀 · ( - 𝑁 · 𝑋 ) ) )
84 19 20 mul2negd ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( - 𝑀 · - 𝑁 ) = ( 𝑀 · 𝑁 ) )
85 84 oveq1d ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( - 𝑀 · - 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑁 ) · 𝑋 ) )
86 85 adantr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( - 𝑀 · - 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑁 ) · 𝑋 ) )
87 33 adantr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → 𝐺 ∈ Grp )
88 3 adantr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → 𝑀 ∈ ℤ )
89 nn0z ( - 𝑁 ∈ ℕ0 → - 𝑁 ∈ ℤ )
90 89 ad2antll ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → - 𝑁 ∈ ℤ )
91 1 2 mulgcl ( ( 𝐺 ∈ Grp ∧ - 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) → ( - 𝑁 · 𝑋 ) ∈ 𝐵 )
92 87 90 81 91 syl3anc ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( - 𝑁 · 𝑋 ) ∈ 𝐵 )
93 1 2 35 mulgneg2 ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ ( - 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( - 𝑀 · ( - 𝑁 · 𝑋 ) ) = ( 𝑀 · ( ( invg𝐺 ) ‘ ( - 𝑁 · 𝑋 ) ) ) )
94 87 88 92 93 syl3anc ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( - 𝑀 · ( - 𝑁 · 𝑋 ) ) = ( 𝑀 · ( ( invg𝐺 ) ‘ ( - 𝑁 · 𝑋 ) ) ) )
95 1 2 35 mulgneg ( ( 𝐺 ∈ Grp ∧ - 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) → ( - - 𝑁 · 𝑋 ) = ( ( invg𝐺 ) ‘ ( - 𝑁 · 𝑋 ) ) )
96 87 90 81 95 syl3anc ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( - - 𝑁 · 𝑋 ) = ( ( invg𝐺 ) ‘ ( - 𝑁 · 𝑋 ) ) )
97 20 negnegd ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → - - 𝑁 = 𝑁 )
98 97 adantr ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → - - 𝑁 = 𝑁 )
99 98 oveq1d ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( - - 𝑁 · 𝑋 ) = ( 𝑁 · 𝑋 ) )
100 96 99 eqtr3d ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( invg𝐺 ) ‘ ( - 𝑁 · 𝑋 ) ) = ( 𝑁 · 𝑋 ) )
101 100 oveq2d ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( 𝑀 · ( ( invg𝐺 ) ‘ ( - 𝑁 · 𝑋 ) ) ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
102 94 101 eqtrd ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( - 𝑀 · ( - 𝑁 · 𝑋 ) ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
103 83 86 102 3eqtr3d ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) ∧ ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
104 103 ex ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
105 18 58 77 104 ccased ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( ( 𝑀 ∈ ℕ0 ∨ - 𝑀 ∈ ℕ0 ) ∧ ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
106 6 10 105 mp2and ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )