Definition df-gsum 17613

Description: Define a finite group sum (also called "iterated sum") of a structure. Given 𝐺 Σ_g 𝐹 where 𝐹:𝐴⟶(Base‘𝐺), the set of indices is 𝐴 and the values are given by 𝐹 at each index. A group sum over a multiplicative group may be viewed as a product. 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 18873.

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 18875 and gsumnunsn 35173.

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

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

Remark: this definition is required here because the symbol Σ_g is already used in df-prds 17618 and df-imas 17680. The related theorems are provided later, see gsumvalx 18865. (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 17611	. 2 class Σg
2		vw	. . 3 setvar 𝑤
3		vf	. . 3 setvar 𝑓
4		cvv 3450	. . 3 class V
5		vo	. . . 4 setvar 𝑜
6		vx	. . . . . . . . . 10 setvar 𝑥
7	6	cv 1568	. . . . . . . . 9 class 𝑥
8		vy	. . . . . . . . . 10 setvar 𝑦
9	8	cv 1568	. . . . . . . . 9 class 𝑦
10	2	cv 1568	. . . . . . . . . 10 class 𝑤
11		cplusg 17428	. . . . . . . . . 10 class +g
12	10, 11	cfv 6538	. . . . . . . . 9 class (+g‘𝑤)
13	7, 9, 12	co 7420	. . . . . . . 8 class (𝑥(+g‘𝑤)𝑦)
14	13, 9	wceq 1569	. . . . . . 7 wff (𝑥(+g‘𝑤)𝑦) = 𝑦
15	9, 7, 12	co 7420	. . . . . . . 8 class (𝑦(+g‘𝑤)𝑥)
16	15, 9	wceq 1569	. . . . . . 7 wff (𝑦(+g‘𝑤)𝑥) = 𝑦
17	14, 16	wa 401	. . . . . 6 wff ((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)
18		cbs 17387	. . . . . . 7 class Base
19	10, 18	cfv 6538	. . . . . 6 class (Base‘𝑤)
20	17, 8, 19	wral 3076	. . . . 5 wff ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)
21	20, 6, 19	crab 3412	. . . 4 class {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)}
22	3	cv 1568	. . . . . . 7 class 𝑓
23	22	crn 5651	. . . . . 6 class ran 𝑓
24	5	cv 1568	. . . . . 6 class 𝑜
25	23, 24	wss 3895	. . . . 5 wff ran 𝑓 ⊆ 𝑜
26		c0g 17610	. . . . . 6 class 0g
27	10, 26	cfv 6538	. . . . 5 class (0g‘𝑤)
28	22	cdm 5650	. . . . . . 7 class dom 𝑓
29		cfz 13639	. . . . . . . 8 class ...
30	29	crn 5651	. . . . . . 7 class ran ...
31	28, 30	wcel 2144	. . . . . 6 wff dom 𝑓 ∈ ran ...
32		vm	. . . . . . . . . . . . 13 setvar 𝑚
33	32	cv 1568	. . . . . . . . . . . 12 class 𝑚
34		vn	. . . . . . . . . . . . 13 setvar 𝑛
35	34	cv 1568	. . . . . . . . . . . 12 class 𝑛
36	33, 35, 29	co 7420	. . . . . . . . . . 11 class (𝑚...𝑛)
37	28, 36	wceq 1569	. . . . . . . . . 10 wff dom 𝑓 = (𝑚...𝑛)
38	12, 22, 33	cseq 14144	. . . . . . . . . . . 12 class seq𝑚((+g‘𝑤), 𝑓)
39	35, 38	cfv 6538	. . . . . . . . . . 11 class (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)
40	7, 39	wceq 1569	. . . . . . . . . 10 wff 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)
41	37, 40	wa 401	. . . . . . . . 9 wff (dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))
42		cuz 12965	. . . . . . . . . 10 class ℤ≥
43	33, 42	cfv 6538	. . . . . . . . 9 class (ℤ≥‘𝑚)
44	41, 34, 43	wrex 3086	. . . . . . . 8 wff ∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))
45	44, 32	wex 1811	. . . . . . 7 wff ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))
46	45, 6	cio 6492	. . . . . 6 class (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)))
47		c1 11201	. . . . . . . . . . . 12 class 1
48		chash 14474	. . . . . . . . . . . . 13 class ♯
49	9, 48	cfv 6538	. . . . . . . . . . . 12 class (♯‘𝑦)
50	47, 49, 29	co 7420	. . . . . . . . . . 11 class (1...(♯‘𝑦))
51		vg	. . . . . . . . . . . 12 setvar 𝑔
52	51	cv 1568	. . . . . . . . . . 11 class 𝑔
53	50, 9, 52	wf1o 6537	. . . . . . . . . 10 wff 𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦
54	22, 52	ccom 5654	. . . . . . . . . . . . 13 class (𝑓 ∘ 𝑔)
55	12, 54, 47	cseq 14144	. . . . . . . . . . . 12 class seq1((+g‘𝑤), (𝑓 ∘ 𝑔))
56	49, 55	cfv 6538	. . . . . . . . . . 11 class (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦))
57	7, 56	wceq 1569	. . . . . . . . . 10 wff 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦))
58	53, 57	wa 401	. . . . . . . . 9 wff (𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦)))
59	22	ccnv 5649	. . . . . . . . . 10 class ◡𝑓
60	4, 24	cdif 4045	. . . . . . . . . 10 class (V ∖ 𝑜)
61	59, 60	cima 5653	. . . . . . . . 9 class (◡𝑓 “ (V ∖ 𝑜))
62	58, 8, 61	wsbc 3738	. . . . . . . 8 wff [(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦)))
63	62, 51	wex 1811	. . . . . . 7 wff ∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦)))
64	63, 6	cio 6492	. . . . . 6 class (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦))))
65	31, 46, 64	cif 4481	. . . . 5 class if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦)))))
66	25, 27, 65	cif 4481	. . . 4 class if(ran 𝑓 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦))))))
67	5, 21, 66	csb 3846	. . 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 7422	. 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 1569	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 used by:  gsumvalx  18865  gsum0  18873