Metamath Proof Explorer

Theorem mulgdirlem

Description: Lemma for mulgdir . (Contributed by Mario Carneiro, 13-Dec-2014)

Ref Expression
Hypotheses mulgnndir.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgnndir.t ⊢ · = ( .g ‘ 𝐺 )
mulgnndir.p ⊢ + = ( +g ‘ 𝐺 )
Assertion mulgdirlem ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 mulgnndir.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgnndir.t ⊢ · = ( .g ‘ 𝐺 )
3 mulgnndir.p ⊢ + = ( +g ‘ 𝐺 )
4 simpl1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → 𝐺 ∈ Grp )
5 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
6 4 5 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → 𝐺 ∈ Mnd )
7 simprl ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑀 ∈ ℕ0 )
8 simprr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℕ0 )
9 simpl23 ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑋 ∈ 𝐵 )
10 1 2 3 mulgnn0dir ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
11 6 7 8 9 10 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
12 11 anassrs ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
13 simpl1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → 𝐺 ∈ Grp )
14 simp22 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → 𝑁 ∈ ℤ )
15 14 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℤ )
16 simpl23 ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → 𝑋 ∈ 𝐵 )
17 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
18 1 2 17 mulgneg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑁 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) )
19 13 15 16 18 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( - 𝑁 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) )
20 19 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( - 𝑁 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) + ( 𝑁 · 𝑋 ) ) )
21 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
22 13 15 16 21 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
23 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
24 1 3 23 17 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) + ( 𝑁 · 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
25 13 22 24 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) + ( 𝑁 · 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
26 20 25 eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( - 𝑁 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
27 26 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( ( 𝑀 + 𝑁 ) · 𝑋 ) + ( ( - 𝑁 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) ) = ( ( ( 𝑀 + 𝑁 ) · 𝑋 ) + ( 0g ‘ 𝐺 ) ) )
28 simpl3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
29 nn0z ⊢ ( ( 𝑀 + 𝑁 ) ∈ ℕ0 → ( 𝑀 + 𝑁 ) ∈ ℤ )
30 28 29 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
31 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) ∈ 𝐵 )
32 13 30 16 31 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) ∈ 𝐵 )
33 1 3 23 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑀 + 𝑁 ) · 𝑋 ) ∈ 𝐵 ) → ( ( ( 𝑀 + 𝑁 ) · 𝑋 ) + ( 0g ‘ 𝐺 ) ) = ( ( 𝑀 + 𝑁 ) · 𝑋 ) )
34 13 32 33 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( ( 𝑀 + 𝑁 ) · 𝑋 ) + ( 0g ‘ 𝐺 ) ) = ( ( 𝑀 + 𝑁 ) · 𝑋 ) )
35 27 34 eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( ( 𝑀 + 𝑁 ) · 𝑋 ) + ( ( - 𝑁 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) ) = ( ( 𝑀 + 𝑁 ) · 𝑋 ) )
36 nn0z ⊢ ( - 𝑁 ∈ ℕ0 → - 𝑁 ∈ ℤ )
37 36 ad2antll ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → - 𝑁 ∈ ℤ )
38 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ - 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑁 · 𝑋 ) ∈ 𝐵 )
39 13 37 16 38 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( - 𝑁 · 𝑋 ) ∈ 𝐵 )
40 1 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( 𝑀 + 𝑁 ) · 𝑋 ) ∈ 𝐵 ∧ ( - 𝑁 · 𝑋 ) ∈ 𝐵 ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) ) → ( ( ( ( 𝑀 + 𝑁 ) · 𝑋 ) + ( - 𝑁 · 𝑋 ) ) + ( 𝑁 · 𝑋 ) ) = ( ( ( 𝑀 + 𝑁 ) · 𝑋 ) + ( ( - 𝑁 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) ) )
41 13 32 39 22 40 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( ( ( 𝑀 + 𝑁 ) · 𝑋 ) + ( - 𝑁 · 𝑋 ) ) + ( 𝑁 · 𝑋 ) ) = ( ( ( 𝑀 + 𝑁 ) · 𝑋 ) + ( ( - 𝑁 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) ) )
42 13 5 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → 𝐺 ∈ Mnd )
43 simprr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → - 𝑁 ∈ ℕ0 )
44 1 2 3 mulgnn0dir ⊢ ( ( 𝐺 ∈ Mnd ∧ ( ( 𝑀 + 𝑁 ) ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( 𝑀 + 𝑁 ) + - 𝑁 ) · 𝑋 ) = ( ( ( 𝑀 + 𝑁 ) · 𝑋 ) + ( - 𝑁 · 𝑋 ) ) )
45 42 28 43 16 44 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( ( 𝑀 + 𝑁 ) + - 𝑁 ) · 𝑋 ) = ( ( ( 𝑀 + 𝑁 ) · 𝑋 ) + ( - 𝑁 · 𝑋 ) ) )
46 simp21 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → 𝑀 ∈ ℤ )
47 46 zcnd ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → 𝑀 ∈ ℂ )
48 14 zcnd ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → 𝑁 ∈ ℂ )
49 47 48 addcld ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℂ )
50 49 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( 𝑀 + 𝑁 ) ∈ ℂ )
51 48 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℂ )
52 50 51 negsubd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 + 𝑁 ) + - 𝑁 ) = ( ( 𝑀 + 𝑁 ) − 𝑁 ) )
53 47 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → 𝑀 ∈ ℂ )
54 53 51 pncand ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
55 52 54 eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 + 𝑁 ) + - 𝑁 ) = 𝑀 )
56 55 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( ( 𝑀 + 𝑁 ) + - 𝑁 ) · 𝑋 ) = ( 𝑀 · 𝑋 ) )
57 45 56 eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( ( 𝑀 + 𝑁 ) · 𝑋 ) + ( - 𝑁 · 𝑋 ) ) = ( 𝑀 · 𝑋 ) )
58 57 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( ( ( 𝑀 + 𝑁 ) · 𝑋 ) + ( - 𝑁 · 𝑋 ) ) + ( 𝑁 · 𝑋 ) ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
59 41 58 eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( ( 𝑀 + 𝑁 ) · 𝑋 ) + ( ( - 𝑁 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
60 35 59 eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
61 60 anassrs ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ 𝑀 ∈ ℕ0 ) ∧ - 𝑁 ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
62 elznn0 ⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) ) )
63 62 simprbi ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) )
64 14 63 syl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) )
65 64 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) )
66 12 61 65 mpjaodan ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
67 simpl1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → 𝐺 ∈ Grp )
68 46 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
69 simpl23 ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
70 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 · 𝑋 ) ∈ 𝐵 )
71 67 68 69 70 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( 𝑀 · 𝑋 ) ∈ 𝐵 )
72 68 znegcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → - 𝑀 ∈ ℤ )
73 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ - 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑀 · 𝑋 ) ∈ 𝐵 )
74 67 72 69 73 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( - 𝑀 · 𝑋 ) ∈ 𝐵 )
75 29 3ad2ant3 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
76 75 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
77 67 76 69 31 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) ∈ 𝐵 )
78 1 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑀 · 𝑋 ) ∈ 𝐵 ∧ ( - 𝑀 · 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑀 + 𝑁 ) · 𝑋 ) ∈ 𝐵 ) ) → ( ( ( 𝑀 · 𝑋 ) + ( - 𝑀 · 𝑋 ) ) + ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) = ( ( 𝑀 · 𝑋 ) + ( ( - 𝑀 · 𝑋 ) + ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) ) )
79 67 71 74 77 78 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( ( 𝑀 · 𝑋 ) + ( - 𝑀 · 𝑋 ) ) + ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) = ( ( 𝑀 · 𝑋 ) + ( ( - 𝑀 · 𝑋 ) + ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) ) )
80 1 2 17 mulgneg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑀 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) )
81 67 68 69 80 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( - 𝑀 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) )
82 81 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( 𝑀 · 𝑋 ) + ( - 𝑀 · 𝑋 ) ) = ( ( 𝑀 · 𝑋 ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) ) )
83 1 3 23 17 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 · 𝑋 ) ∈ 𝐵 ) → ( ( 𝑀 · 𝑋 ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) ) = ( 0g ‘ 𝐺 ) )
84 67 71 83 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( 𝑀 · 𝑋 ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) ) = ( 0g ‘ 𝐺 ) )
85 82 84 eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( 𝑀 · 𝑋 ) + ( - 𝑀 · 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
86 85 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( ( 𝑀 · 𝑋 ) + ( - 𝑀 · 𝑋 ) ) + ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) = ( ( 0g ‘ 𝐺 ) + ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) )
87 1 3 23 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑀 + 𝑁 ) · 𝑋 ) ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) = ( ( 𝑀 + 𝑁 ) · 𝑋 ) )
88 67 77 87 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( 0g ‘ 𝐺 ) + ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) = ( ( 𝑀 + 𝑁 ) · 𝑋 ) )
89 86 88 eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( ( 𝑀 · 𝑋 ) + ( - 𝑀 · 𝑋 ) ) + ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) = ( ( 𝑀 + 𝑁 ) · 𝑋 ) )
90 67 5 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → 𝐺 ∈ Mnd )
91 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → - 𝑀 ∈ ℕ0 )
92 simpl3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
93 1 2 3 mulgnn0dir ⊢ ( ( 𝐺 ∈ Mnd ∧ ( - 𝑀 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( - 𝑀 + ( 𝑀 + 𝑁 ) ) · 𝑋 ) = ( ( - 𝑀 · 𝑋 ) + ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) )
94 90 91 92 69 93 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( - 𝑀 + ( 𝑀 + 𝑁 ) ) · 𝑋 ) = ( ( - 𝑀 · 𝑋 ) + ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) )
95 47 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℂ )
96 95 negcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → - 𝑀 ∈ ℂ )
97 49 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℂ )
98 96 97 addcomd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( - 𝑀 + ( 𝑀 + 𝑁 ) ) = ( ( 𝑀 + 𝑁 ) + - 𝑀 ) )
99 97 95 negsubd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) + - 𝑀 ) = ( ( 𝑀 + 𝑁 ) − 𝑀 ) )
100 48 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
101 95 100 pncan2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) − 𝑀 ) = 𝑁 )
102 98 99 101 3eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( - 𝑀 + ( 𝑀 + 𝑁 ) ) = 𝑁 )
103 102 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( - 𝑀 + ( 𝑀 + 𝑁 ) ) · 𝑋 ) = ( 𝑁 · 𝑋 ) )
104 94 103 eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( - 𝑀 · 𝑋 ) + ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) = ( 𝑁 · 𝑋 ) )
105 104 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( 𝑀 · 𝑋 ) + ( ( - 𝑀 · 𝑋 ) + ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
106 79 89 105 3eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
107 elznn0 ⊢ ( 𝑀 ∈ ℤ ↔ ( 𝑀 ∈ ℝ ∧ ( 𝑀 ∈ ℕ0 ∨ - 𝑀 ∈ ℕ0 ) ) )
108 107 simprbi ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ∈ ℕ0 ∨ - 𝑀 ∈ ℕ0 ) )
109 46 108 syl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝑀 ∈ ℕ0 ∨ - 𝑀 ∈ ℕ0 ) )
110 66 106 109 mpjaodan ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )