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		grpmnd	$⊢ G \in Grp \to G \in Mnd$
6	4 5	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 G \in Mnd$
7		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}$
8		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}$
9		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$
10	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)$
11	6 7 8 9 10	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)$
12	11	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)$
13		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$
14		simp22	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B) \land M + N \in ℕ_{0}) \to N \in ℤ$
15	14	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 ℤ$
16		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$
17		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
18	1 2 17	mulgneg	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to -N \underset{˙}{\cdot} X = {inv}_{g} (G) (N \underset{˙}{\cdot} X)$
19	13 15 16 18	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)$
20	19	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)$
21	1 2	mulgcl	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to N \underset{˙}{\cdot} X \in B$
22	13 15 16 21	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$
23		eqid	$⊢ 0_{G} = 0_{G}$
24	1 3 23 17	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}$
25	13 22 24	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}$
26	20 25	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}$
27	26	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}$
28		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}$
29		nn0z	$⊢ M + N \in ℕ_{0} \to M + N \in ℤ$
30	28 29	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 ℤ$
31	1 2	mulgcl	$⊢ (G \in Grp \land M + N \in ℤ \land X \in B) \to (M + N) \underset{˙}{\cdot} X \in B$
32	13 30 16 31	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$
33	1 3 23	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$
34	13 32 33	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$
35	27 34	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$
36		nn0z	$⊢ - N \in ℕ_{0} \to - N \in ℤ$
37	36	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 ℤ$
38	1 2	mulgcl	$⊢ (G \in Grp \land - N \in ℤ \land X \in B) \to -N \underset{˙}{\cdot} X \in B$
39	13 37 16 38	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$
40	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))$
41	13 32 39 22 40	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))$
42	13 5	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 G \in Mnd$
43		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}$
44	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)$
45	42 28 43 16 44	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)$
46		simp21	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B) \land M + N \in ℕ_{0}) \to M \in ℤ$
47	46	zcnd	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B) \land M + N \in ℕ_{0}) \to M \in ℂ$
48	14	zcnd	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B) \land M + N \in ℕ_{0}) \to N \in ℂ$
49	47 48	addcld	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B) \land M + N \in ℕ_{0}) \to M + N \in ℂ$
50	49	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 ℂ$
51	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 N \in ℂ$
52	50 51	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$
53	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 M \in ℂ$
54	53 51	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$
55	52 54	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$
56	55	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$
57	45 56	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$
58	57	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)$
59	41 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) \underset{˙}{+} ((-N \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X)) = (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X)$
60	35 59	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)$
61	60	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)$
62		elznn0	$⊢ N \in ℤ \leftrightarrow (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0}))$
63	62	simprbi	$⊢ N \in ℤ \to (N \in ℕ_{0} \lor - N \in ℕ_{0})$
64	14 63	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})$
65	64	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})$
66	12 61 65	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)$
67		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$
68	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 ℤ$
69		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$
70	1 2	mulgcl	$⊢ (G \in Grp \land M \in ℤ \land X \in B) \to M \underset{˙}{\cdot} X \in B$
71	67 68 69 70	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$
72	68	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 ℤ$
73	1 2	mulgcl	$⊢ (G \in Grp \land - M \in ℤ \land X \in B) \to -M \underset{˙}{\cdot} X \in B$
74	67 72 69 73	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$
75	29	3ad2ant3	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B) \land M + N \in ℕ_{0}) \to M + N \in ℤ$
76	75	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 ℤ$
77	67 76 69 31	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$
78	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))$
79	67 71 74 77 78	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))$
80	1 2 17	mulgneg	$⊢ (G \in Grp \land M \in ℤ \land X \in B) \to -M \underset{˙}{\cdot} X = {inv}_{g} (G) (M \underset{˙}{\cdot} X)$
81	67 68 69 80	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)$
82	81	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)$
83	1 3 23 17	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}$
84	67 71 83	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}$
85	82 84	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}$
86	85	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)$
87	1 3 23	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$
88	67 77 87	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$
89	86 88	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$
90	67 5	syl	$⊢ ((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$
91		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}$
92		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}$
93	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)$
94	90 91 92 69 93	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)$
95	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 M \in ℂ$
96	95	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 ℂ$
97	49	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 ℂ$
98	96 97	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$
99	97 95	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$
100	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 N \in ℂ$
101	95 100	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$
102	98 99 101	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$
103	102	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$
104	94 103	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$
105	104	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)$
106	79 89 105	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)$
107		elznn0	$⊢ M \in ℤ \leftrightarrow (M \in ℝ \land (M \in ℕ_{0} \lor - M \in ℕ_{0}))$
108	107	simprbi	$⊢ M \in ℤ \to (M \in ℕ_{0} \lor - M \in ℕ_{0})$
109	46 108	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})$
110	66 106 109	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