mulgdirlem

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

Proof

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

Metamath Proof Explorer

Theorem mulgdirlem

Proof