mulgnn0di

Description: Group multiple of a sum, for nonnegative multiples. (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	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)$

Proof

Step	Hyp	Ref	Expression
1		mulgdi.b	$⊢ B = {Base}_{G}$
2		mulgdi.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulgdi.p	$⊢ \underset{˙}{+} = +_{G}$
4		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
5	4	ad2antrr	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \to G \in Mnd$
6	1 3	mndcl	$⊢ (G \in Mnd \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
7	6	3expb	$⊢ (G \in Mnd \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
8	5 7	sylan	$⊢ (((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
9	1 3	cmncom	$⊢ (G \in CMnd \land x \in B \land y \in B) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
10	9	3expb	$⊢ (G \in CMnd \land (x \in B \land y \in B)) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
11	10	ad4ant14	$⊢ (((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \land (x \in B \land y \in B)) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
12	1 3	mndass	$⊢ (G \in Mnd \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
13	5 12	sylan	$⊢ (((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
14		simpr	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \to M \in ℕ$
15		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
16	14 15	eleqtrdi	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \to M \in ℤ_{\geq 1}$
17		simplr2	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \to X \in B$
18		elfznn	$⊢ k \in (1 \dots M) \to k \in ℕ$
19		fvconst2g	$⊢ (X \in B \land k \in ℕ) \to (ℕ \times \{X\}) (k) = X$
20	17 18 19	syl2an	$⊢ (((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \land k \in (1 \dots M)) \to (ℕ \times \{X\}) (k) = X$
21	17	adantr	$⊢ (((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \land k \in (1 \dots M)) \to X \in B$
22	20 21	eqeltrd	$⊢ (((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \land k \in (1 \dots M)) \to (ℕ \times \{X\}) (k) \in B$
23		simplr3	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \to Y \in B$
24		fvconst2g	$⊢ (Y \in B \land k \in ℕ) \to (ℕ \times \{Y\}) (k) = Y$
25	23 18 24	syl2an	$⊢ (((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \land k \in (1 \dots M)) \to (ℕ \times \{Y\}) (k) = Y$
26	23	adantr	$⊢ (((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \land k \in (1 \dots M)) \to Y \in B$
27	25 26	eqeltrd	$⊢ (((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \land k \in (1 \dots M)) \to (ℕ \times \{Y\}) (k) \in B$
28	1 3	mndcl	$⊢ (G \in Mnd \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$
29	5 17 23 28	syl3anc	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \to X \underset{˙}{+} Y \in B$
30		fvconst2g	$⊢ (X \underset{˙}{+} Y \in B \land k \in ℕ) \to (ℕ \times \{X \underset{˙}{+} Y\}) (k) = X \underset{˙}{+} Y$
31	29 18 30	syl2an	$⊢ (((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \land k \in (1 \dots M)) \to (ℕ \times \{X \underset{˙}{+} Y\}) (k) = X \underset{˙}{+} Y$
32	20 25	oveq12d	$⊢ (((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \land k \in (1 \dots M)) \to (ℕ \times \{X\}) (k) \underset{˙}{+} (ℕ \times \{Y\}) (k) = X \underset{˙}{+} Y$
33	31 32	eqtr4d	$⊢ (((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \land k \in (1 \dots M)) \to (ℕ \times \{X \underset{˙}{+} Y\}) (k) = (ℕ \times \{X\}) (k) \underset{˙}{+} (ℕ \times \{Y\}) (k)$
34	8 11 13 16 22 27 33	seqcaopr	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \to seq 1 (\underset{˙}{+}, (ℕ \times \{X \underset{˙}{+} Y\})) (M) = seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (M) \underset{˙}{+} seq 1 (\underset{˙}{+}, (ℕ \times \{Y\})) (M)$
35		eqid	$⊢ seq 1 (\underset{˙}{+}, (ℕ \times \{X \underset{˙}{+} Y\})) = seq 1 (\underset{˙}{+}, (ℕ \times \{X \underset{˙}{+} Y\}))$
36	1 3 2 35	mulgnn	$⊢ (M \in ℕ \land X \underset{˙}{+} Y \in B) \to M \underset{˙}{\cdot} (X \underset{˙}{+} Y) = seq 1 (\underset{˙}{+}, (ℕ \times \{X \underset{˙}{+} Y\})) (M)$
37	14 29 36	syl2anc	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \to M \underset{˙}{\cdot} (X \underset{˙}{+} Y) = seq 1 (\underset{˙}{+}, (ℕ \times \{X \underset{˙}{+} Y\})) (M)$
38		eqid	$⊢ seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) = seq 1 (\underset{˙}{+}, (ℕ \times \{X\}))$
39	1 3 2 38	mulgnn	$⊢ (M \in ℕ \land X \in B) \to M \underset{˙}{\cdot} X = seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (M)$
40	14 17 39	syl2anc	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \to M \underset{˙}{\cdot} X = seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (M)$
41		eqid	$⊢ seq 1 (\underset{˙}{+}, (ℕ \times \{Y\})) = seq 1 (\underset{˙}{+}, (ℕ \times \{Y\}))$
42	1 3 2 41	mulgnn	$⊢ (M \in ℕ \land Y \in B) \to M \underset{˙}{\cdot} Y = seq 1 (\underset{˙}{+}, (ℕ \times \{Y\})) (M)$
43	14 23 42	syl2anc	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \to M \underset{˙}{\cdot} Y = seq 1 (\underset{˙}{+}, (ℕ \times \{Y\})) (M)$
44	40 43	oveq12d	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \to (M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y) = seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (M) \underset{˙}{+} seq 1 (\underset{˙}{+}, (ℕ \times \{Y\})) (M)$
45	34 37 44	3eqtr4d	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M \in ℕ) \to M \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y)$
46	4	ad2antrr	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to G \in Mnd$
47		simplr2	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to X \in B$
48		simplr3	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to Y \in B$
49	46 47 48 28	syl3anc	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to X \underset{˙}{+} Y \in B$
50		eqid	$⊢ 0_{G} = 0_{G}$
51	1 50 2	mulg0	$⊢ X \underset{˙}{+} Y \in B \to 0 \underset{˙}{\cdot} (X \underset{˙}{+} Y) = 0_{G}$
52	49 51	syl	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to 0 \underset{˙}{\cdot} (X \underset{˙}{+} Y) = 0_{G}$
53		eqid	$⊢ {Base}_{G} = {Base}_{G}$
54	53 50	mndidcl	$⊢ G \in Mnd \to 0_{G} \in {Base}_{G}$
55	53 3 50	mndlid	$⊢ (G \in Mnd \land 0_{G} \in {Base}_{G}) \to 0_{G} \underset{˙}{+} 0_{G} = 0_{G}$
56	4 54 55	syl2anc2	$⊢ G \in CMnd \to 0_{G} \underset{˙}{+} 0_{G} = 0_{G}$
57	56	ad2antrr	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to 0_{G} \underset{˙}{+} 0_{G} = 0_{G}$
58	52 57	eqtr4d	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to 0 \underset{˙}{\cdot} (X \underset{˙}{+} Y) = 0_{G} \underset{˙}{+} 0_{G}$
59		simpr	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to M = 0$
60	59	oveq1d	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to M \underset{˙}{\cdot} (X \underset{˙}{+} Y) = 0 \underset{˙}{\cdot} (X \underset{˙}{+} Y)$
61	59	oveq1d	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to M \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
62	1 50 2	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = 0_{G}$
63	47 62	syl	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to 0 \underset{˙}{\cdot} X = 0_{G}$
64	61 63	eqtrd	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to M \underset{˙}{\cdot} X = 0_{G}$
65	59	oveq1d	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to M \underset{˙}{\cdot} Y = 0 \underset{˙}{\cdot} Y$
66	1 50 2	mulg0	$⊢ Y \in B \to 0 \underset{˙}{\cdot} Y = 0_{G}$
67	48 66	syl	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to 0 \underset{˙}{\cdot} Y = 0_{G}$
68	65 67	eqtrd	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to M \underset{˙}{\cdot} Y = 0_{G}$
69	64 68	oveq12d	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to (M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y) = 0_{G} \underset{˙}{+} 0_{G}$
70	58 60 69	3eqtr4d	$⊢ ((G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \land M = 0) \to M \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (M \underset{˙}{\cdot} X) \underset{˙}{+} (M \underset{˙}{\cdot} Y)$
71		simpr1	$⊢ (G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \to M \in ℕ_{0}$
72		elnn0	$⊢ M \in ℕ_{0} \leftrightarrow (M \in ℕ \lor M = 0)$
73	71 72	sylib	$⊢ (G \in CMnd \land (M \in ℕ_{0} \land X \in B \land Y \in B)) \to (M \in ℕ \lor M = 0)$
74	45 70 73	mpjaodan	$⊢ (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)$

Metamath Proof Explorer

Theorem mulgnn0di

Proof