Definition df-gsum 16103

Description: Define the group sum for the structure 𝐺 of a finite sequence of elements whose values are defined by the expression 𝐵 and whose set of indices is 𝐴. It may be viewed as a product (if 𝐺 is a multiplication), a sum (if 𝐺 is an addition) or whatever. The variable 𝑘 is normally a free variable in 𝐵 ( i.e. 𝐵 can be thought of as 𝐵(𝑘)). The definition is meaningful in different contexts, depending on the size of the index set 𝐴 and each demanding different properties of 𝐺.

1. If 𝐴 = ∅ and 𝐺 has an identity element, then the sum equals this identity.

2. If 𝐴 = (𝑀...𝑁) and 𝐺 is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e. (𝐵(1) + 𝐵(2)) + 𝐵(3) etc.

3. If 𝐴 is a finite set (or is nonzero for finitely many indices) and 𝐺 is a commutative monoid, then the sum adds up these elements in some order, which is then uniquely defined.

4. If 𝐴 is an infinite set and 𝐺 is a Hausdorff topological group, then there is a meaningful sum, but Σ_g cannot handle this case. See df-tsms 21930. Remark: this definition is required here because the symbol Σ_g is already used in df-prds 16108 and df-imas 16168. The related theorems are provided later, see gsumvalx 17270. (Contributed by FL, 5-Sep-2010.) (Revised by FL, 17-Oct-2011.) (Revised by Mario Carneiro, 7-Dec-2014.)

Assertion

Ref	Expression
df-gsum	⊢ Σg = (𝑤 ∈ V, 𝑓 ∈ V ↦ ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑓 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(#‘𝑦)))))))

Distinct variable group:   𝑓,𝑔,𝑚,𝑛,𝑜,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-gsum

Step	Hyp	Ref	Expression
1		cgsu 16101	. 2 class Σg
2		vw	. . 3 setvar 𝑤
3		vf	. . 3 setvar 𝑓
4		cvv 3200	. . 3 class V
5		vo	. . . 4 setvar 𝑜
6		vx	. . . . . . . . . 10 setvar 𝑥
7	6	cv 1482	. . . . . . . . 9 class 𝑥
8		vy	. . . . . . . . . 10 setvar 𝑦
9	8	cv 1482	. . . . . . . . 9 class 𝑦
10	2	cv 1482	. . . . . . . . . 10 class 𝑤
11		cplusg 15941	. . . . . . . . . 10 class +g
12	10, 11	cfv 5888	. . . . . . . . 9 class (+g‘𝑤)
13	7, 9, 12	co 6650	. . . . . . . 8 class (𝑥(+g‘𝑤)𝑦)
14	13, 9	wceq 1483	. . . . . . 7 wff (𝑥(+g‘𝑤)𝑦) = 𝑦
15	9, 7, 12	co 6650	. . . . . . . 8 class (𝑦(+g‘𝑤)𝑥)
16	15, 9	wceq 1483	. . . . . . 7 wff (𝑦(+g‘𝑤)𝑥) = 𝑦
17	14, 16	wa 384	. . . . . 6 wff ((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)
18		cbs 15857	. . . . . . 7 class Base
19	10, 18	cfv 5888	. . . . . 6 class (Base‘𝑤)
20	17, 8, 19	wral 2912	. . . . 5 wff ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)
21	20, 6, 19	crab 2916	. . . 4 class {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)}
22	3	cv 1482	. . . . . . 7 class 𝑓
23	22	crn 5115	. . . . . 6 class ran 𝑓
24	5	cv 1482	. . . . . 6 class 𝑜
25	23, 24	wss 3574	. . . . 5 wff ran 𝑓 ⊆ 𝑜
26		c0g 16100	. . . . . 6 class 0g
27	10, 26	cfv 5888	. . . . 5 class (0g‘𝑤)
28	22	cdm 5114	. . . . . . 7 class dom 𝑓
29		cfz 12326	. . . . . . . 8 class ...
30	29	crn 5115	. . . . . . 7 class ran ...
31	28, 30	wcel 1990	. . . . . 6 wff dom 𝑓 ∈ ran ...
32		vm	. . . . . . . . . . . . 13 setvar 𝑚
33	32	cv 1482	. . . . . . . . . . . 12 class 𝑚
34		vn	. . . . . . . . . . . . 13 setvar 𝑛
35	34	cv 1482	. . . . . . . . . . . 12 class 𝑛
36	33, 35, 29	co 6650	. . . . . . . . . . 11 class (𝑚...𝑛)
37	28, 36	wceq 1483	. . . . . . . . . 10 wff dom 𝑓 = (𝑚...𝑛)
38	12, 22, 33	cseq 12801	. . . . . . . . . . . 12 class seq𝑚((+g‘𝑤), 𝑓)
39	35, 38	cfv 5888	. . . . . . . . . . 11 class (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)
40	7, 39	wceq 1483	. . . . . . . . . 10 wff 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)
41	37, 40	wa 384	. . . . . . . . 9 wff (dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))
42		cuz 11687	. . . . . . . . . 10 class ℤ≥
43	33, 42	cfv 5888	. . . . . . . . 9 class (ℤ≥‘𝑚)
44	41, 34, 43	wrex 2913	. . . . . . . 8 wff ∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))
45	44, 32	wex 1704	. . . . . . 7 wff ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))
46	45, 6	cio 5849	. . . . . 6 class (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)))
47		c1 9937	. . . . . . . . . . . 12 class 1
48		chash 13117	. . . . . . . . . . . . 13 class #
49	9, 48	cfv 5888	. . . . . . . . . . . 12 class (#‘𝑦)
50	47, 49, 29	co 6650	. . . . . . . . . . 11 class (1...(#‘𝑦))
51		vg	. . . . . . . . . . . 12 setvar 𝑔
52	51	cv 1482	. . . . . . . . . . 11 class 𝑔
53	50, 9, 52	wf1o 5887	. . . . . . . . . 10 wff 𝑔:(1...(#‘𝑦))–1-1-onto→𝑦
54	22, 52	ccom 5118	. . . . . . . . . . . . 13 class (𝑓 ∘ 𝑔)
55	12, 54, 47	cseq 12801	. . . . . . . . . . . 12 class seq1((+g‘𝑤), (𝑓 ∘ 𝑔))
56	49, 55	cfv 5888	. . . . . . . . . . 11 class (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(#‘𝑦))
57	7, 56	wceq 1483	. . . . . . . . . 10 wff 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(#‘𝑦))
58	53, 57	wa 384	. . . . . . . . 9 wff (𝑔:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(#‘𝑦)))
59	22	ccnv 5113	. . . . . . . . . 10 class ◡𝑓
60	4, 24	cdif 3571	. . . . . . . . . 10 class (V ∖ 𝑜)
61	59, 60	cima 5117	. . . . . . . . 9 class (◡𝑓 “ (V ∖ 𝑜))
62	58, 8, 61	wsbc 3435	. . . . . . . 8 wff [(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(#‘𝑦)))
63	62, 51	wex 1704	. . . . . . 7 wff ∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(#‘𝑦)))
64	63, 6	cio 5849	. . . . . 6 class (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(#‘𝑦))))
65	31, 46, 64	cif 4086	. . . . 5 class if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(#‘𝑦)))))
66	25, 27, 65	cif 4086	. . . 4 class if(ran 𝑓 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(#‘𝑦))))))
67	5, 21, 66	csb 3533	. . 3 class ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑓 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(#‘𝑦))))))
68	2, 3, 4, 4, 67	cmpt2 6652	. 2 class (𝑤 ∈ V, 𝑓 ∈ V ↦ ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑓 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(#‘𝑦)))))))
69	1, 68	wceq 1483	1 wff Σg = (𝑤 ∈ V, 𝑓 ∈ V ↦ ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑓 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(#‘𝑦)))))))

This definition is referenced by:  gsumvalx  17270  gsum0  17278