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

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