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

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 imbitrid ⊢ ( ( 𝐺 ∈ 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 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )