mulgnndir

Description: Sum of group multiples, for positive multiples. (Contributed by Mario Carneiro, 11-Dec-2014) (Revised by AV, 29-Aug-2021)

	Ref	Expression
Hypotheses	mulgnndir.b	$⊢ B = {Base}_{G}$
	mulgnndir.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mulgnndir.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	mulgnndir	$⊢ (G \in Smgrp \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		sgrpmgm	$⊢ G \in Smgrp \to G \in Mgm$
5	1 3	mgmcl	$⊢ (G \in Mgm \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
6	4 5	syl3an1	$⊢ (G \in Smgrp \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
7	6	3expb	$⊢ (G \in Smgrp \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
8	7	adantlr	$⊢ ((G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
9	1 3	sgrpass	$⊢ (G \in Smgrp \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
10	9	adantlr	$⊢ ((G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
11		simpr2	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to N \in ℕ$
12		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
13	11 12	eleqtrdi	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to N \in ℤ_{\geq 1}$
14		simpr1	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to M \in ℕ$
15	14	nnzd	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to M \in ℤ$
16		eluzadd	$⊢ (N \in ℤ_{\geq 1} \land M \in ℤ) \to N + M \in ℤ_{\geq (1 + M)}$
17	13 15 16	syl2anc	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to N + M \in ℤ_{\geq (1 + M)}$
18	14	nncnd	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to M \in ℂ$
19	11	nncnd	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to N \in ℂ$
20	18 19	addcomd	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to M + N = N + M$
21		ax-1cn	$⊢ 1 \in ℂ$
22		addcom	$⊢ (M \in ℂ \land 1 \in ℂ) \to M + 1 = 1 + M$
23	18 21 22	sylancl	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to M + 1 = 1 + M$
24	23	fveq2d	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to ℤ_{\geq (M + 1)} = ℤ_{\geq (1 + M)}$
25	17 20 24	3eltr4d	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to M + N \in ℤ_{\geq (M + 1)}$
26	14 12	eleqtrdi	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to M \in ℤ_{\geq 1}$
27		simpr3	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to X \in B$
28		elfznn	$⊢ x \in (1 \dots M + N) \to x \in ℕ$
29		fvconst2g	$⊢ (X \in B \land x \in ℕ) \to (ℕ \times \{X\}) (x) = X$
30	27 28 29	syl2an	$⊢ ((G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \land x \in (1 \dots M + N)) \to (ℕ \times \{X\}) (x) = X$
31	27	adantr	$⊢ ((G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \land x \in (1 \dots M + N)) \to X \in B$
32	30 31	eqeltrd	$⊢ ((G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \land x \in (1 \dots M + N)) \to (ℕ \times \{X\}) (x) \in B$
33	8 10 25 26 32	seqsplit	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (M + N) = seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (M) \underset{˙}{+} seq (M + 1) (\underset{˙}{+}, (ℕ \times \{X\})) (M + N)$
34		nnaddcl	$⊢ (M \in ℕ \land N \in ℕ) \to M + N \in ℕ$
35	14 11 34	syl2anc	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to M + N \in ℕ$
36		eqid	$⊢ seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) = seq 1 (\underset{˙}{+}, (ℕ \times \{X\}))$
37	1 3 2 36	mulgnn	$⊢ (M + N \in ℕ \land X \in B) \to (M + N) \underset{˙}{\cdot} X = seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (M + N)$
38	35 27 37	syl2anc	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to (M + N) \underset{˙}{\cdot} X = seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (M + N)$
39	1 3 2 36	mulgnn	$⊢ (M \in ℕ \land X \in B) \to M \underset{˙}{\cdot} X = seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (M)$
40	14 27 39	syl2anc	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to M \underset{˙}{\cdot} X = seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (M)$
41		elfznn	$⊢ x \in (1 \dots N) \to x \in ℕ$
42	27 41 29	syl2an	$⊢ ((G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \land x \in (1 \dots N)) \to (ℕ \times \{X\}) (x) = X$
43	27	adantr	$⊢ ((G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \land x \in (1 \dots N)) \to X \in B$
44		nnaddcl	$⊢ (x \in ℕ \land M \in ℕ) \to x + M \in ℕ$
45	41 14 44	syl2anr	$⊢ ((G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \land x \in (1 \dots N)) \to x + M \in ℕ$
46		fvconst2g	$⊢ (X \in B \land x + M \in ℕ) \to (ℕ \times \{X\}) (x + M) = X$
47	43 45 46	syl2anc	$⊢ ((G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \land x \in (1 \dots N)) \to (ℕ \times \{X\}) (x + M) = X$
48	42 47	eqtr4d	$⊢ ((G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \land x \in (1 \dots N)) \to (ℕ \times \{X\}) (x) = (ℕ \times \{X\}) (x + M)$
49	13 15 48	seqshft2	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (N) = seq (1 + M) (\underset{˙}{+}, (ℕ \times \{X\})) (N + M)$
50	1 3 2 36	mulgnn	$⊢ (N \in ℕ \land X \in B) \to N \underset{˙}{\cdot} X = seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (N)$
51	11 27 50	syl2anc	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to N \underset{˙}{\cdot} X = seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (N)$
52	23	seqeq1d	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to seq (M + 1) (\underset{˙}{+}, (ℕ \times \{X\})) = seq (1 + M) (\underset{˙}{+}, (ℕ \times \{X\}))$
53	52 20	fveq12d	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to seq (M + 1) (\underset{˙}{+}, (ℕ \times \{X\})) (M + N) = seq (1 + M) (\underset{˙}{+}, (ℕ \times \{X\})) (N + M)$
54	49 51 53	3eqtr4d	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to N \underset{˙}{\cdot} X = seq (M + 1) (\underset{˙}{+}, (ℕ \times \{X\})) (M + N)$
55	40 54	oveq12d	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X) = seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (M) \underset{˙}{+} seq (M + 1) (\underset{˙}{+}, (ℕ \times \{X\})) (M + N)$
56	33 38 55	3eqtr4d	$⊢ (G \in Smgrp \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 mulgnndir

Proof