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