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 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )