gsumconst

Description: Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Mario Carneiro, 24-Apr-2016)

	Ref	Expression
Hypotheses	gsumconst.b	$⊢ B = {Base}_{G}$
	gsumconst.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	gsumconst	$⊢ (G \in Mnd \land A \in Fin \land X \in B) \to \underset{k \in A}{\sum_{G}} X = \|A\| \underset{˙}{\cdot} X$

Proof

Step	Hyp	Ref	Expression
1		gsumconst.b	$⊢ B = {Base}_{G}$
2		gsumconst.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		simpl3	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land A = \emptyset) \to X \in B$
4		eqid	$⊢ 0_{G} = 0_{G}$
5	1 4 2	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = 0_{G}$
6	3 5	syl	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land A = \emptyset) \to 0 \underset{˙}{\cdot} X = 0_{G}$
7		fveq2	$⊢ A = \emptyset \to \|A\| = \|\emptyset\|$
8	7	adantl	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land A = \emptyset) \to \|A\| = \|\emptyset\|$
9		hash0	$⊢ \|\emptyset\| = 0$
10	8 9	eqtrdi	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land A = \emptyset) \to \|A\| = 0$
11	10	oveq1d	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land A = \emptyset) \to \|A\| \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
12		mpteq1	$⊢ A = \emptyset \to (k \in A ⟼ X) = (k \in \emptyset ⟼ X)$
13	12	adantl	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land A = \emptyset) \to (k \in A ⟼ X) = (k \in \emptyset ⟼ X)$
14		mpt0	$⊢ (k \in \emptyset ⟼ X) = \emptyset$
15	13 14	eqtrdi	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land A = \emptyset) \to (k \in A ⟼ X) = \emptyset$
16	15	oveq2d	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land A = \emptyset) \to \underset{k \in A}{\sum_{G}} X = \sum_{G} \emptyset$
17	4	gsum0	$⊢ \sum_{G} \emptyset = 0_{G}$
18	16 17	eqtrdi	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land A = \emptyset) \to \underset{k \in A}{\sum_{G}} X = 0_{G}$
19	6 11 18	3eqtr4rd	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land A = \emptyset) \to \underset{k \in A}{\sum_{G}} X = \|A\| \underset{˙}{\cdot} X$
20	19	ex	$⊢ (G \in Mnd \land A \in Fin \land X \in B) \to (A = \emptyset \to \underset{k \in A}{\sum_{G}} X = \|A\| \underset{˙}{\cdot} X)$
21		simprl	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℕ$
22		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
23	21 22	eleqtrdi	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℤ_{\geq 1}$
24		simpr	$⊢ (((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to x \in (1 \dots \|A\|)$
25		simpl3	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to X \in B$
26	25	adantr	$⊢ (((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to X \in B$
27		eqid	$⊢ (x \in (1 \dots \|A\|) ⟼ X) = (x \in (1 \dots \|A\|) ⟼ X)$
28	27	fvmpt2	$⊢ (x \in (1 \dots \|A\|) \land X \in B) \to (x \in (1 \dots \|A\|) ⟼ X) (x) = X$
29	24 26 28	syl2anc	$⊢ (((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to (x \in (1 \dots \|A\|) ⟼ X) (x) = X$
30		f1of	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : (1 \dots \|A\|) ⟶ A$
31	30	ad2antll	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) ⟶ A$
32	31	ffvelcdmda	$⊢ (((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to f (x) \in A$
33	31	feqmptd	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f = (x \in (1 \dots \|A\|) ⟼ f (x))$
34		eqidd	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ X) = (k \in A ⟼ X)$
35		eqidd	$⊢ k = f (x) \to X = X$
36	32 33 34 35	fmptco	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ X) \circ f = (x \in (1 \dots \|A\|) ⟼ X)$
37	36	fveq1d	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ((k \in A ⟼ X) \circ f) (x) = (x \in (1 \dots \|A\|) ⟼ X) (x)$
38	37	adantr	$⊢ (((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to ((k \in A ⟼ X) \circ f) (x) = (x \in (1 \dots \|A\|) ⟼ X) (x)$
39		elfznn	$⊢ x \in (1 \dots \|A\|) \to x \in ℕ$
40		fvconst2g	$⊢ (X \in B \land x \in ℕ) \to (ℕ \times \{X\}) (x) = X$
41	25 39 40	syl2an	$⊢ (((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to (ℕ \times \{X\}) (x) = X$
42	29 38 41	3eqtr4d	$⊢ (((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to ((k \in A ⟼ X) \circ f) (x) = (ℕ \times \{X\}) (x)$
43	23 42	seqfveq	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to seq 1 (+_{G}, ((k \in A ⟼ X) \circ f)) (\|A\|) = seq 1 (+_{G}, (ℕ \times \{X\})) (\|A\|)$
44		eqid	$⊢ +_{G} = +_{G}$
45		eqid	$⊢ Cntz (G) = Cntz (G)$
46		simpl1	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to G \in Mnd$
47		simpl2	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to A \in Fin$
48	25	adantr	$⊢ (((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land k \in A) \to X \in B$
49	48	fmpttd	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ X) : A ⟶ B$
50		eqidd	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to X +_{G} X = X +_{G} X$
51	1 44 45	elcntzsn	$⊢ X \in B \to (X \in Cntz (G) (\{X\}) \leftrightarrow (X \in B \land X +_{G} X = X +_{G} X))$
52	25 51	syl	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (X \in Cntz (G) (\{X\}) \leftrightarrow (X \in B \land X +_{G} X = X +_{G} X))$
53	25 50 52	mpbir2and	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to X \in Cntz (G) (\{X\})$
54	53	snssd	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \{X\} \subseteq Cntz (G) (\{X\})$
55		snidg	$⊢ X \in B \to X \in \{X\}$
56	25 55	syl	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to X \in \{X\}$
57	56	adantr	$⊢ (((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land k \in A) \to X \in \{X\}$
58	57	fmpttd	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ X) : A ⟶ \{X\}$
59	58	frnd	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ran (k \in A ⟼ X) \subseteq \{X\}$
60	45	cntzidss	$⊢ (\{X\} \subseteq Cntz (G) (\{X\}) \land ran (k \in A ⟼ X) \subseteq \{X\}) \to ran (k \in A ⟼ X) \subseteq Cntz (G) (ran (k \in A ⟼ X))$
61	54 59 60	syl2anc	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ran (k \in A ⟼ X) \subseteq Cntz (G) (ran (k \in A ⟼ X))$
62		f1of1	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : (1 \dots \|A\|) \underset{1-1}{⟶} A$
63	62	ad2antll	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) \underset{1-1}{⟶} A$
64		suppssdm	$⊢ (k \in A ⟼ X) supp 0_{G} \subseteq dom (k \in A ⟼ X)$
65		eqid	$⊢ (k \in A ⟼ X) = (k \in A ⟼ X)$
66	65	dmmptss	$⊢ dom (k \in A ⟼ X) \subseteq A$
67	66	a1i	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to dom (k \in A ⟼ X) \subseteq A$
68	64 67	sstrid	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ X) supp 0_{G} \subseteq A$
69		f1ofo	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : (1 \dots \|A\|) \underset{onto}{⟶} A$
70		forn	$⊢ f : (1 \dots \|A\|) \underset{onto}{⟶} A \to ran f = A$
71	69 70	syl	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to ran f = A$
72	71	ad2antll	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ran f = A$
73	68 72	sseqtrrd	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ X) supp 0_{G} \subseteq ran f$
74		eqid	$⊢ ((k \in A ⟼ X) \circ f) supp 0_{G} = ((k \in A ⟼ X) \circ f) supp 0_{G}$
75	1 4 44 45 46 47 49 61 21 63 73 74	gsumval3	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \underset{k \in A}{\sum_{G}} X = seq 1 (+_{G}, ((k \in A ⟼ X) \circ f)) (\|A\|)$
76		eqid	$⊢ seq 1 (+_{G}, (ℕ \times \{X\})) = seq 1 (+_{G}, (ℕ \times \{X\}))$
77	1 44 2 76	mulgnn	$⊢ (\|A\| \in ℕ \land X \in B) \to \|A\| \underset{˙}{\cdot} X = seq 1 (+_{G}, (ℕ \times \{X\})) (\|A\|)$
78	21 25 77	syl2anc	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \underset{˙}{\cdot} X = seq 1 (+_{G}, (ℕ \times \{X\})) (\|A\|)$
79	43 75 78	3eqtr4d	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \underset{k \in A}{\sum_{G}} X = \|A\| \underset{˙}{\cdot} X$
80	79	expr	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land \|A\| \in ℕ) \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \underset{k \in A}{\sum_{G}} X = \|A\| \underset{˙}{\cdot} X)$
81	80	exlimdv	$⊢ ((G \in Mnd \land A \in Fin \land X \in B) \land \|A\| \in ℕ) \to (\exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \underset{k \in A}{\sum_{G}} X = \|A\| \underset{˙}{\cdot} X)$
82	81	expimpd	$⊢ (G \in Mnd \land A \in Fin \land X \in B) \to ((\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \underset{k \in A}{\sum_{G}} X = \|A\| \underset{˙}{\cdot} X)$
83		fz1f1o	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
84	83	3ad2ant2	$⊢ (G \in Mnd \land A \in Fin \land X \in B) \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
85	20 82 84	mpjaod	$⊢ (G \in Mnd \land A \in Fin \land X \in B) \to \underset{k \in A}{\sum_{G}} X = \|A\| \underset{˙}{\cdot} X$

Metamath Proof Explorer

Theorem gsumconst

Proof