mulgdir

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

	Ref	Expression
Hypotheses	mulgnndir.b	$⊢ B = {Base}_{G}$
	mulgnndir.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mulgnndir.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	mulgdir	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \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	1 2 3	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)$
5	4	3expa	$⊢ ((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)$
6		simpll	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to G \in Grp$
7		simpr2	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to N \in ℤ$
8	7	adantr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to N \in ℤ$
9	8	znegcld	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to - N \in ℤ$
10		simpr1	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to M \in ℤ$
11	10	adantr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to M \in ℤ$
12	11	znegcld	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to - M \in ℤ$
13		simplr3	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to X \in B$
14	11	zcnd	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to M \in ℂ$
15	14	negcld	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to - M \in ℂ$
16	8	zcnd	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to N \in ℂ$
17	16	negcld	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to - N \in ℂ$
18	14 16	negdid	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to - (M + N) = - M + -N$
19	15 17 18	comraddd	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to - (M + N) = - N + -M$
20		simpr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to - (M + N) \in ℕ_{0}$
21	19 20	eqeltrrd	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to - N + -M \in ℕ_{0}$
22	1 2 3	mulgdirlem	$⊢ (G \in Grp \land (- N \in ℤ \land - M \in ℤ \land X \in B) \land - N + -M \in ℕ_{0}) \to (- N + -M) \underset{˙}{\cdot} X = (-N \underset{˙}{\cdot} X) \underset{˙}{+} (-M \underset{˙}{\cdot} X)$
23	6 9 12 13 21 22	syl131anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to (- N + -M) \underset{˙}{\cdot} X = (-N \underset{˙}{\cdot} X) \underset{˙}{+} (-M \underset{˙}{\cdot} X)$
24	19	oveq1d	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to (- (M + N)) \underset{˙}{\cdot} X = (- N + -M) \underset{˙}{\cdot} X$
25	10 7	zaddcld	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to M + N \in ℤ$
26	25	adantr	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to M + N \in ℤ$
27		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
28	1 2 27	mulgneg	$⊢ (G \in Grp \land M + N \in ℤ \land X \in B) \to (- (M + N)) \underset{˙}{\cdot} X = {inv}_{g} (G) ((M + N) \underset{˙}{\cdot} X)$
29	6 26 13 28	syl3anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to (- (M + N)) \underset{˙}{\cdot} X = {inv}_{g} (G) ((M + N) \underset{˙}{\cdot} X)$
30	24 29	eqtr3d	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to (- N + -M) \underset{˙}{\cdot} X = {inv}_{g} (G) ((M + N) \underset{˙}{\cdot} X)$
31	1 2 27	mulgneg	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to -N \underset{˙}{\cdot} X = {inv}_{g} (G) (N \underset{˙}{\cdot} X)$
32	6 8 13 31	syl3anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to -N \underset{˙}{\cdot} X = {inv}_{g} (G) (N \underset{˙}{\cdot} X)$
33	1 2 27	mulgneg	$⊢ (G \in Grp \land M \in ℤ \land X \in B) \to -M \underset{˙}{\cdot} X = {inv}_{g} (G) (M \underset{˙}{\cdot} X)$
34	6 11 13 33	syl3anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to -M \underset{˙}{\cdot} X = {inv}_{g} (G) (M \underset{˙}{\cdot} X)$
35	32 34	oveq12d	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to (-N \underset{˙}{\cdot} X) \underset{˙}{+} (-M \underset{˙}{\cdot} X) = {inv}_{g} (G) (N \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (M \underset{˙}{\cdot} X)$
36	1 2	mulgcl	$⊢ (G \in Grp \land M \in ℤ \land X \in B) \to M \underset{˙}{\cdot} X \in B$
37	6 11 13 36	syl3anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to M \underset{˙}{\cdot} X \in B$
38	1 2	mulgcl	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to N \underset{˙}{\cdot} X \in B$
39	6 8 13 38	syl3anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to N \underset{˙}{\cdot} X \in B$
40	1 3 27	grpinvadd	$⊢ (G \in Grp \land M \underset{˙}{\cdot} X \in B \land N \underset{˙}{\cdot} X \in B) \to {inv}_{g} (G) ((M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X)) = {inv}_{g} (G) (N \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (M \underset{˙}{\cdot} X)$
41	6 37 39 40	syl3anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to {inv}_{g} (G) ((M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X)) = {inv}_{g} (G) (N \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (M \underset{˙}{\cdot} X)$
42	35 41	eqtr4d	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to (-N \underset{˙}{\cdot} X) \underset{˙}{+} (-M \underset{˙}{\cdot} X) = {inv}_{g} (G) ((M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X))$
43	23 30 42	3eqtr3d	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to {inv}_{g} (G) ((M + N) \underset{˙}{\cdot} X) = {inv}_{g} (G) ((M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X))$
44	43	fveq2d	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to {inv}_{g} (G) ({inv}_{g} (G) ((M + N) \underset{˙}{\cdot} X)) = {inv}_{g} (G) ({inv}_{g} (G) ((M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X)))$
45	1 2	mulgcl	$⊢ (G \in Grp \land M + N \in ℤ \land X \in B) \to (M + N) \underset{˙}{\cdot} X \in B$
46	6 26 13 45	syl3anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to (M + N) \underset{˙}{\cdot} X \in B$
47	1 27	grpinvinv	$⊢ (G \in Grp \land (M + N) \underset{˙}{\cdot} X \in B) \to {inv}_{g} (G) ({inv}_{g} (G) ((M + N) \underset{˙}{\cdot} X)) = (M + N) \underset{˙}{\cdot} X$
48	6 46 47	syl2anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to {inv}_{g} (G) ({inv}_{g} (G) ((M + N) \underset{˙}{\cdot} X)) = (M + N) \underset{˙}{\cdot} X$
49	1 3	grpcl	$⊢ (G \in Grp \land M \underset{˙}{\cdot} X \in B \land N \underset{˙}{\cdot} X \in B) \to (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X) \in B$
50	6 37 39 49	syl3anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X) \in B$
51	1 27	grpinvinv	$⊢ (G \in Grp \land (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X) \in B) \to {inv}_{g} (G) ({inv}_{g} (G) ((M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X))) = (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X)$
52	6 50 51	syl2anc	$⊢ ((G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \land - (M + N) \in ℕ_{0}) \to {inv}_{g} (G) ({inv}_{g} (G) ((M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X))) = (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X)$
53	44 48 52	3eqtr3d	$⊢ ((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)$
54		elznn0	$⊢ M + N \in ℤ \leftrightarrow (M + N \in ℝ \land (M + N \in ℕ_{0} \lor - (M + N) \in ℕ_{0}))$
55	54	simprbi	$⊢ M + N \in ℤ \to (M + N \in ℕ_{0} \lor - (M + N) \in ℕ_{0})$
56	25 55	syl	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to (M + N \in ℕ_{0} \lor - (M + N) \in ℕ_{0})$
57	5 53 56	mpjaodan	$⊢ (G \in Grp \land (M \in ℤ \land N \in ℤ \land X \in B)) \to (M + N) \underset{˙}{\cdot} X = (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem mulgdir

Proof