mulgdi

Description: Group multiple of a sum. (Contributed by Mario Carneiro, 13-Dec-2014)

	Ref	Expression
Hypotheses	mulgdi.b	$⊢ B = {Base}_{G}$
	mulgdi.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mulgdi.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	mulgdi	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to M \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y)$

Proof

Step	Hyp	Ref	Expression
1		mulgdi.b	$⊢ B = {Base}_{G}$
2		mulgdi.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulgdi.p	$⊢ \underset{˙}{+} = +_{G}$
4		ablcmn	$⊢ G \in Abel \to G \in CMnd$
5	4	ad2antrr	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land M \in ℕ_{0}) \to G \in CMnd$
6		simpr	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land M \in ℕ_{0}) \to M \in ℕ_{0}$
7		simplr2	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land M \in ℕ_{0}) \to X \in B$
8		simplr3	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land M \in ℕ_{0}) \to Y \in B$
9	1 2 3	mulgnn0di	$⊢ (G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \to M \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y)$
10	5 6 7 8 9	syl13anc	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land M \in ℕ_{0}) \to M \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y)$
11	4	ad2antrr	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to G \in CMnd$
12		simpr	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to - M \in ℕ_{0}$
13		simpr2	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to X \in B$
14	13	adantr	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to X \in B$
15		simpr3	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to Y \in B$
16	15	adantr	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to Y \in B$
17	1 2 3	mulgnn0di	$⊢ (G \in CMnd \land (- M \in ℕ_{0} \land X \in B \land Y \in B)) \to -M \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (-M \underset{˙}{\cdot} X) \underset{˙}{+} (-M \underset{˙}{\cdot} Y)$
18	11 12 14 16 17	syl13anc	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to -M \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (-M \underset{˙}{\cdot} X) \underset{˙}{+} (-M \underset{˙}{\cdot} Y)$
19		ablgrp	$⊢ G \in Abel \to G \in Grp$
20	19	adantr	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to G \in Grp$
21		simpr1	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to M \in ℤ$
22	1 3	grpcl	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$
23	20 13 15 22	syl3anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to X \underset{˙}{+} Y \in B$
24		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
25	1 2 24	mulgneg	$⊢ (G \in Grp \land M \in ℤ \land X \underset{˙}{+} Y \in B) \to -M \underset{˙}{\cdot} (X \underset{˙}{+} Y) = {inv}_{g} (G) (M \underset{˙}{\cdot} (X \underset{˙}{+} Y))$
26	20 21 23 25	syl3anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to -M \underset{˙}{\cdot} (X \underset{˙}{+} Y) = {inv}_{g} (G) (M \underset{˙}{\cdot} (X \underset{˙}{+} Y))$
27	26	adantr	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to -M \underset{˙}{\cdot} (X \underset{˙}{+} Y) = {inv}_{g} (G) (M \underset{˙}{\cdot} (X \underset{˙}{+} Y))$
28	1 2 24	mulgneg	$⊢ (G \in Grp \land M \in ℤ \land X \in B) \to -M \underset{˙}{\cdot} X = {inv}_{g} (G) (M \underset{˙}{\cdot} X)$
29	20 21 13 28	syl3anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to -M \underset{˙}{\cdot} X = {inv}_{g} (G) (M \underset{˙}{\cdot} X)$
30	1 2 24	mulgneg	$⊢ (G \in Grp \land M \in ℤ \land Y \in B) \to -M \underset{˙}{\cdot} Y = {inv}_{g} (G) (M \underset{˙}{\cdot} Y)$
31	20 21 15 30	syl3anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to -M \underset{˙}{\cdot} Y = {inv}_{g} (G) (M \underset{˙}{\cdot} Y)$
32	29 31	oveq12d	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to (-M \underset{˙}{\cdot} X) \underset{˙}{+} (-M \underset{˙}{\cdot} Y) = {inv}_{g} (G) (M \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (M \underset{˙}{\cdot} Y)$
33	32	adantr	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to (-M \underset{˙}{\cdot} X) \underset{˙}{+} (-M \underset{˙}{\cdot} Y) = {inv}_{g} (G) (M \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (M \underset{˙}{\cdot} Y)$
34	18 27 33	3eqtr3d	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to {inv}_{g} (G) (M \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = {inv}_{g} (G) (M \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (M \underset{˙}{\cdot} Y)$
35		simpl	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to G \in Abel$
36	1 2	mulgcl	$⊢ (G \in Grp \land M \in ℤ \land X \in B) \to M \underset{˙}{\cdot} X \in B$
37	20 21 13 36	syl3anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to M \underset{˙}{\cdot} X \in B$
38	1 2	mulgcl	$⊢ (G \in Grp \land M \in ℤ \land Y \in B) \to M \underset{˙}{\cdot} Y \in B$
39	20 21 15 38	syl3anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to M \underset{˙}{\cdot} Y \in B$
40	1 3 24	ablinvadd	$⊢ (G \in Abel \land M \underset{˙}{\cdot} X \in B \land M \underset{˙}{\cdot} Y \in B) \to {inv}_{g} (G) ((M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y)) = {inv}_{g} (G) (M \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (M \underset{˙}{\cdot} Y)$
41	35 37 39 40	syl3anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to {inv}_{g} (G) ((M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y)) = {inv}_{g} (G) (M \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (M \underset{˙}{\cdot} Y)$
42	41	adantr	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to {inv}_{g} (G) ((M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y)) = {inv}_{g} (G) (M \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (M \underset{˙}{\cdot} Y)$
43	34 42	eqtr4d	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to {inv}_{g} (G) (M \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = {inv}_{g} (G) ((M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y))$
44	43	fveq2d	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to {inv}_{g} (G) ({inv}_{g} (G) (M \underset{˙}{\cdot} (X \underset{˙}{+} Y))) = {inv}_{g} (G) ({inv}_{g} (G) ((M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y)))$
45	1 2	mulgcl	$⊢ (G \in Grp \land M \in ℤ \land X \underset{˙}{+} Y \in B) \to M \underset{˙}{\cdot} (X \underset{˙}{+} Y) \in B$
46	20 21 23 45	syl3anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to M \underset{˙}{\cdot} (X \underset{˙}{+} Y) \in B$
47	46	adantr	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to M \underset{˙}{\cdot} (X \underset{˙}{+} Y) \in B$
48	1 24	grpinvinv	$⊢ (G \in Grp \land M \underset{˙}{\cdot} (X \underset{˙}{+} Y) \in B) \to {inv}_{g} (G) ({inv}_{g} (G) (M \underset{˙}{\cdot} (X \underset{˙}{+} Y))) = M \underset{˙}{\cdot} (X \underset{˙}{+} Y)$
49	20 47 48	syl2an2r	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to {inv}_{g} (G) ({inv}_{g} (G) (M \underset{˙}{\cdot} (X \underset{˙}{+} Y))) = M \underset{˙}{\cdot} (X \underset{˙}{+} Y)$
50	1 3	grpcl	$⊢ (G \in Grp \land M \underset{˙}{\cdot} X \in B \land M \underset{˙}{\cdot} Y \in B) \to (M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y) \in B$
51	20 37 39 50	syl3anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to (M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y) \in B$
52	51	adantr	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to (M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y) \in B$
53	1 24	grpinvinv	$⊢ (G \in Grp \land (M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y) \in B) \to {inv}_{g} (G) ({inv}_{g} (G) ((M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y))) = (M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y)$
54	20 52 53	syl2an2r	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to {inv}_{g} (G) ({inv}_{g} (G) ((M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y))) = (M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y)$
55	44 49 54	3eqtr3d	$⊢ ((G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \land - M \in ℕ_{0}) \to M \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y)$
56		elznn0	$⊢ M \in ℤ \leftrightarrow (M \in ℝ \land (M \in ℕ_{0} \lor - M \in ℕ_{0}))$
57	56	simprbi	$⊢ M \in ℤ \to (M \in ℕ_{0} \lor - M \in ℕ_{0})$
58	21 57	syl	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to (M \in ℕ_{0} \lor - M \in ℕ_{0})$
59	10 55 58	mpjaodan	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to M \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y)$

Metamath Proof Explorer

Theorem mulgdi

Proof