mulgass

Description: Product of group multiples, generalized to ZZ . (Contributed by Mario Carneiro, 13-Dec-2014)

	Ref	Expression
Hypotheses	mulgass.b	$⊢ B = {Base}_{G}$
	mulgass.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	mulgass	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$

Proof

Step	Hyp	Ref	Expression
1		mulgass.b	$⊢ B = {Base}_{G}$
2		mulgass.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		simpr1	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to M \in ℤ$
4		elznn0	$⊢ M \in ℤ \leftrightarrow (M \in ℝ \land (M \in ℕ_{0} \lor - M \in ℕ_{0}))$
5	4	simprbi	$⊢ M \in ℤ \to (M \in ℕ_{0} \lor - M \in ℕ_{0})$
6	3 5	syl	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to (M \in ℕ_{0} \lor - M \in ℕ_{0})$
7		simpr2	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to N \in ℤ$
8		elznn0	$⊢ N \in ℤ \leftrightarrow (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0}))$
9	8	simprbi	$⊢ N \in ℤ \to (N \in ℕ_{0} \lor - N \in ℕ_{0})$
10	7 9	syl	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to (N \in ℕ_{0} \lor - N \in ℕ_{0})$
11		grpmnd	$⊢ G \in Grp \to G \in Mnd$
12	11	ad2antrr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to G \in Mnd$
13		simprl	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to M \in ℕ_{0}$
14		simprr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to N \in ℕ_{0}$
15		simplr3	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to X \in B$
16	1 2	mulgnn0ass	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
17	12 13 14 15 16	syl13anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
18	17	ex	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
19	3	zcnd	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to M \in ℂ$
20	7	zcnd	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to N \in ℂ$
21	19 20	mulneg1d	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to -M \cdot N = - M \cdot N$
22	21	adantr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land N \in ℕ_{0})) \to -M \cdot N = - M \cdot N$
23	22	oveq1d	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land N \in ℕ_{0})) \to -M \cdot N \underset{˙}{\cdot} X = (- M \cdot N) \underset{˙}{\cdot} X$
24	11	ad2antrr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land N \in ℕ_{0})) \to G \in Mnd$
25		simprl	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land N \in ℕ_{0})) \to - M \in ℕ_{0}$
26		simprr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land N \in ℕ_{0})) \to N \in ℕ_{0}$
27		simpr3	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to X \in B$
28	27	adantr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land N \in ℕ_{0})) \to X \in B$
29	1 2	mulgnn0ass	$⊢ (G \in Mnd \land (- M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to -M \cdot N \underset{˙}{\cdot} X = -M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
30	24 25 26 28 29	syl13anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land N \in ℕ_{0})) \to -M \cdot N \underset{˙}{\cdot} X = -M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
31	23 30	eqtr3d	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land N \in ℕ_{0})) \to (- M \cdot N) \underset{˙}{\cdot} X = -M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
32		fveq2	$⊢ (- M \cdot N) \underset{˙}{\cdot} X = -M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) \to {inv}_{g} (G) ((- M \cdot N) \underset{˙}{\cdot} X) = {inv}_{g} (G) (-M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
33		simpl	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to G \in Grp$
34	3 7	zmulcld	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to M \cdot N \in ℤ$
35		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
36	1 2 35	mulgneg	$⊢ (G \in Grp \land M \cdot N \in ℤ \land X \in B) \to (- M \cdot N) \underset{˙}{\cdot} X = {inv}_{g} (G) (M \cdot N \underset{˙}{\cdot} X)$
37	33 34 27 36	syl3anc	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to (- M \cdot N) \underset{˙}{\cdot} X = {inv}_{g} (G) (M \cdot N \underset{˙}{\cdot} X)$
38	37	fveq2d	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to {inv}_{g} (G) ((- M \cdot N) \underset{˙}{\cdot} X) = {inv}_{g} (G) ({inv}_{g} (G) (M \cdot N \underset{˙}{\cdot} X))$
39	1 2	mulgcl	$⊢ (G \in Grp \land M \cdot N \in ℤ \land X \in B) \to M \cdot N \underset{˙}{\cdot} X \in B$
40	33 34 27 39	syl3anc	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to M \cdot N \underset{˙}{\cdot} X \in B$
41	1 35	grpinvinv	$⊢ (G \in Grp \land M \cdot N \underset{˙}{\cdot} X \in B) \to {inv}_{g} (G) ({inv}_{g} (G) (M \cdot N \underset{˙}{\cdot} X)) = M \cdot N \underset{˙}{\cdot} X$
42	40 41	syldan	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to {inv}_{g} (G) ({inv}_{g} (G) (M \cdot N \underset{˙}{\cdot} X)) = M \cdot N \underset{˙}{\cdot} X$
43	38 42	eqtrd	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to {inv}_{g} (G) ((- M \cdot N) \underset{˙}{\cdot} X) = M \cdot N \underset{˙}{\cdot} X$
44	1 2	mulgcl	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to N \underset{˙}{\cdot} X \in B$
45	33 7 27 44	syl3anc	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to N \underset{˙}{\cdot} X \in B$
46	1 2 35	mulgneg	$⊢ (G \in Grp \land M \in ℤ \land N \underset{˙}{\cdot} X \in B) \to -M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = {inv}_{g} (G) (M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
47	33 3 45 46	syl3anc	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to -M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = {inv}_{g} (G) (M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
48	47	fveq2d	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to {inv}_{g} (G) (-M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)) = {inv}_{g} (G) ({inv}_{g} (G) (M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)))$
49	1 2	mulgcl	$⊢ (G \in Grp \land M \in ℤ \land N \underset{˙}{\cdot} X \in B) \to M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) \in B$
50	33 3 45 49	syl3anc	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) \in B$
51	1 35	grpinvinv	$⊢ (G \in Grp \land M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) \in B) \to {inv}_{g} (G) ({inv}_{g} (G) (M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))) = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
52	50 51	syldan	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to {inv}_{g} (G) ({inv}_{g} (G) (M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))) = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
53	48 52	eqtrd	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to {inv}_{g} (G) (-M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)) = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
54	43 53	eqeq12d	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to ({inv}_{g} (G) ((- M \cdot N) \underset{˙}{\cdot} X) = {inv}_{g} (G) (-M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)) \leftrightarrow M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
55	32 54	imbitrid	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to ((- M \cdot N) \underset{˙}{\cdot} X = -M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
56	55	imp	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \cdot N) \underset{˙}{\cdot} X = -M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
57	31 56	syldan	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land N \in ℕ_{0})) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
58	57	ex	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to ((- M \in ℕ_{0} \land N \in ℕ_{0}) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
59	11	ad2antrr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (M \in ℕ_{0} \land - N \in ℕ_{0})) \to G \in Mnd$
60		simprl	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (M \in ℕ_{0} \land - N \in ℕ_{0})) \to M \in ℕ_{0}$
61		simprr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (M \in ℕ_{0} \land - N \in ℕ_{0})) \to - N \in ℕ_{0}$
62	27	adantr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (M \in ℕ_{0} \land - N \in ℕ_{0})) \to X \in B$
63	1 2	mulgnn0ass	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land - N \in ℕ_{0} \land X \in B)) \to M -N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (-N \underset{˙}{\cdot} X)$
64	59 60 61 62 63	syl13anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (M \in ℕ_{0} \land - N \in ℕ_{0})) \to M -N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (-N \underset{˙}{\cdot} X)$
65	19 20	mulneg2d	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to M -N = - M \cdot N$
66	65	adantr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (M \in ℕ_{0} \land - N \in ℕ_{0})) \to M -N = - M \cdot N$
67	66	oveq1d	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (M \in ℕ_{0} \land - N \in ℕ_{0})) \to M -N \underset{˙}{\cdot} X = (- M \cdot N) \underset{˙}{\cdot} X$
68	1 2 35	mulgneg	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to -N \underset{˙}{\cdot} X = {inv}_{g} (G) (N \underset{˙}{\cdot} X)$
69	33 7 27 68	syl3anc	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to -N \underset{˙}{\cdot} X = {inv}_{g} (G) (N \underset{˙}{\cdot} X)$
70	69	oveq2d	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to M \underset{˙}{\cdot} (-N \underset{˙}{\cdot} X) = M \underset{˙}{\cdot} {inv}_{g} (G) (N \underset{˙}{\cdot} X)$
71	1 2 35	mulgneg2	$⊢ (G \in Grp \land M \in ℤ \land N \underset{˙}{\cdot} X \in B) \to -M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = M \underset{˙}{\cdot} {inv}_{g} (G) (N \underset{˙}{\cdot} X)$
72	33 3 45 71	syl3anc	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to -M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = M \underset{˙}{\cdot} {inv}_{g} (G) (N \underset{˙}{\cdot} X)$
73	70 72	eqtr4d	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to M \underset{˙}{\cdot} (-N \underset{˙}{\cdot} X) = -M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
74	73	adantr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (M \in ℕ_{0} \land - N \in ℕ_{0})) \to M \underset{˙}{\cdot} (-N \underset{˙}{\cdot} X) = -M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
75	64 67 74	3eqtr3d	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (M \in ℕ_{0} \land - N \in ℕ_{0})) \to (- M \cdot N) \underset{˙}{\cdot} X = -M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
76	75 56	syldan	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (M \in ℕ_{0} \land - N \in ℕ_{0})) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
77	76	ex	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to ((M \in ℕ_{0} \land - N \in ℕ_{0}) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
78	11	ad2antrr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to G \in Mnd$
79		simprl	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to - M \in ℕ_{0}$
80		simprr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to - N \in ℕ_{0}$
81	27	adantr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to X \in B$
82	1 2	mulgnn0ass	$⊢ (G \in Mnd \land (- M \in ℕ_{0} \land - N \in ℕ_{0} \land X \in B)) \to -M -N \underset{˙}{\cdot} X = -M \underset{˙}{\cdot} (-N \underset{˙}{\cdot} X)$
83	78 79 80 81 82	syl13anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to -M -N \underset{˙}{\cdot} X = -M \underset{˙}{\cdot} (-N \underset{˙}{\cdot} X)$
84	19 20	mul2negd	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to -M -N = M \cdot N$
85	84	oveq1d	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to -M -N \underset{˙}{\cdot} X = M \cdot N \underset{˙}{\cdot} X$
86	85	adantr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to -M -N \underset{˙}{\cdot} X = M \cdot N \underset{˙}{\cdot} X$
87	33	adantr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to G \in Grp$
88	3	adantr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to M \in ℤ$
89		nn0z	$⊢ - N \in ℕ_{0} \to - N \in ℤ$
90	89	ad2antll	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to - N \in ℤ$
91	1 2	mulgcl	$⊢ (G \in Grp \land - N \in ℤ \land X \in B) \to -N \underset{˙}{\cdot} X \in B$
92	87 90 81 91	syl3anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to -N \underset{˙}{\cdot} X \in B$
93	1 2 35	mulgneg2	$⊢ (G \in Grp \land M \in ℤ \land -N \underset{˙}{\cdot} X \in B) \to -M \underset{˙}{\cdot} (-N \underset{˙}{\cdot} X) = M \underset{˙}{\cdot} {inv}_{g} (G) (-N \underset{˙}{\cdot} X)$
94	87 88 92 93	syl3anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to -M \underset{˙}{\cdot} (-N \underset{˙}{\cdot} X) = M \underset{˙}{\cdot} {inv}_{g} (G) (-N \underset{˙}{\cdot} X)$
95	1 2 35	mulgneg	$⊢ (G \in Grp \land - N \in ℤ \land X \in B) \to (- -N) \underset{˙}{\cdot} X = {inv}_{g} (G) (-N \underset{˙}{\cdot} X)$
96	87 90 81 95	syl3anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to (- -N) \underset{˙}{\cdot} X = {inv}_{g} (G) (-N \underset{˙}{\cdot} X)$
97	20	negnegd	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to - -N = N$
98	97	adantr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to - -N = N$
99	98	oveq1d	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to (- -N) \underset{˙}{\cdot} X = N \underset{˙}{\cdot} X$
100	96 99	eqtr3d	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to {inv}_{g} (G) (-N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} X$
101	100	oveq2d	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to M \underset{˙}{\cdot} {inv}_{g} (G) (-N \underset{˙}{\cdot} X) = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
102	94 101	eqtrd	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to -M \underset{˙}{\cdot} (-N \underset{˙}{\cdot} X) = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
103	83 86 102	3eqtr3d	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land (- M \in ℕ_{0} \land - N \in ℕ_{0})) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
104	103	ex	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to ((- M \in ℕ_{0} \land - N \in ℕ_{0}) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
105	18 58 77 104	ccased	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to (((M \in ℕ_{0} \lor - M \in ℕ_{0}) \land (N \in ℕ_{0} \lor - N \in ℕ_{0})) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
106	6 10 105	mp2and	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem mulgass

Proof