Definition df-gsum 17070

Description: Define the group sum (also called "iterated 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 any other operation. 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. See gsum0 18283.

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. See gsumval2 18285 and gsumnunsn 32420.

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. See gsumval3 19423.

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 23186.

Remark: this definition is required here because the symbol Σ_g is already used in df-prds 17075 and df-imas 17136. The related theorems are provided later, see gsumvalx 18275. (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 17068	. 2 class Σg
2		vw	. . 3 setvar 𝑤
3		vf	. . 3 setvar 𝑓
4		cvv 3422	. . 3 class V
5		vo	. . . 4 setvar 𝑜
6		vx	. . . . . . . . . 10 setvar 𝑥
7	6	cv 1538	. . . . . . . . 9 class 𝑥
8		vy	. . . . . . . . . 10 setvar 𝑦
9	8	cv 1538	. . . . . . . . 9 class 𝑦
10	2	cv 1538	. . . . . . . . . 10 class 𝑤
11		cplusg 16888	. . . . . . . . . 10 class +g
12	10, 11	cfv 6418	. . . . . . . . 9 class (+g‘𝑤)
13	7, 9, 12	co 7255	. . . . . . . 8 class (𝑥(+g‘𝑤)𝑦)
14	13, 9	wceq 1539	. . . . . . 7 wff (𝑥(+g‘𝑤)𝑦) = 𝑦
15	9, 7, 12	co 7255	. . . . . . . 8 class (𝑦(+g‘𝑤)𝑥)
16	15, 9	wceq 1539	. . . . . . 7 wff (𝑦(+g‘𝑤)𝑥) = 𝑦
17	14, 16	wa 395	. . . . . 6 wff ((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)
18		cbs 16840	. . . . . . 7 class Base
19	10, 18	cfv 6418	. . . . . 6 class (Base‘𝑤)
20	17, 8, 19	wral 3063	. . . . 5 wff ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)
21	20, 6, 19	crab 3067	. . . 4 class {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)}
22	3	cv 1538	. . . . . . 7 class 𝑓
23	22	crn 5581	. . . . . 6 class ran 𝑓
24	5	cv 1538	. . . . . 6 class 𝑜
25	23, 24	wss 3883	. . . . 5 wff ran 𝑓 ⊆ 𝑜
26		c0g 17067	. . . . . 6 class 0g
27	10, 26	cfv 6418	. . . . 5 class (0g‘𝑤)
28	22	cdm 5580	. . . . . . 7 class dom 𝑓
29		cfz 13168	. . . . . . . 8 class ...
30	29	crn 5581	. . . . . . 7 class ran ...
31	28, 30	wcel 2108	. . . . . 6 wff dom 𝑓 ∈ ran ...
32		vm	. . . . . . . . . . . . 13 setvar 𝑚
33	32	cv 1538	. . . . . . . . . . . 12 class 𝑚
34		vn	. . . . . . . . . . . . 13 setvar 𝑛
35	34	cv 1538	. . . . . . . . . . . 12 class 𝑛
36	33, 35, 29	co 7255	. . . . . . . . . . 11 class (𝑚...𝑛)
37	28, 36	wceq 1539	. . . . . . . . . 10 wff dom 𝑓 = (𝑚...𝑛)
38	12, 22, 33	cseq 13649	. . . . . . . . . . . 12 class seq𝑚((+g‘𝑤), 𝑓)
39	35, 38	cfv 6418	. . . . . . . . . . 11 class (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)
40	7, 39	wceq 1539	. . . . . . . . . 10 wff 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)
41	37, 40	wa 395	. . . . . . . . 9 wff (dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))
42		cuz 12511	. . . . . . . . . 10 class ℤ≥
43	33, 42	cfv 6418	. . . . . . . . 9 class (ℤ≥‘𝑚)
44	41, 34, 43	wrex 3064	. . . . . . . 8 wff ∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))
45	44, 32	wex 1783	. . . . . . 7 wff ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))
46	45, 6	cio 6374	. . . . . 6 class (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)))
47		c1 10803	. . . . . . . . . . . 12 class 1
48		chash 13972	. . . . . . . . . . . . 13 class ♯
49	9, 48	cfv 6418	. . . . . . . . . . . 12 class (♯‘𝑦)
50	47, 49, 29	co 7255	. . . . . . . . . . 11 class (1...(♯‘𝑦))
51		vg	. . . . . . . . . . . 12 setvar 𝑔
52	51	cv 1538	. . . . . . . . . . 11 class 𝑔
53	50, 9, 52	wf1o 6417	. . . . . . . . . 10 wff 𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦
54	22, 52	ccom 5584	. . . . . . . . . . . . 13 class (𝑓 ∘ 𝑔)
55	12, 54, 47	cseq 13649	. . . . . . . . . . . 12 class seq1((+g‘𝑤), (𝑓 ∘ 𝑔))
56	49, 55	cfv 6418	. . . . . . . . . . 11 class (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦))
57	7, 56	wceq 1539	. . . . . . . . . 10 wff 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦))
58	53, 57	wa 395	. . . . . . . . 9 wff (𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦)))
59	22	ccnv 5579	. . . . . . . . . 10 class ◡𝑓
60	4, 24	cdif 3880	. . . . . . . . . 10 class (V ∖ 𝑜)
61	59, 60	cima 5583	. . . . . . . . 9 class (◡𝑓 “ (V ∖ 𝑜))
62	58, 8, 61	wsbc 3711	. . . . . . . 8 wff [(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦)))
63	62, 51	wex 1783	. . . . . . 7 wff ∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦)))
64	63, 6	cio 6374	. . . . . 6 class (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦))))
65	31, 46, 64	cif 4456	. . . . 5 class if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦)))))
66	25, 27, 65	cif 4456	. . . 4 class if(ran 𝑓 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦))))))
67	5, 21, 66	csb 3828	. . 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	cmpo 7257	. 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 1539	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  18275  gsum0  18283