MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-gsum Structured version   Visualization version   GIF version

Definition df-gsum 16706
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 17884.

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 17886 and gsumnunsn 31711.

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

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

Remark: this definition is required here because the symbol Σg is already used in df-prds 16711 and df-imas 16771. The related theorems are provided later, see gsumvalx 17876. (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
StepHypRef Expression
1 cgsu 16704 . 2 class Σg
2 vw . . 3 setvar 𝑤
3 vf . . 3 setvar 𝑓
4 cvv 3495 . . 3 class V
5 vo . . . 4 setvar 𝑜
6 vx . . . . . . . . . 10 setvar 𝑥
76cv 1527 . . . . . . . . 9 class 𝑥
8 vy . . . . . . . . . 10 setvar 𝑦
98cv 1527 . . . . . . . . 9 class 𝑦
102cv 1527 . . . . . . . . . 10 class 𝑤
11 cplusg 16555 . . . . . . . . . 10 class +g
1210, 11cfv 6349 . . . . . . . . 9 class (+g𝑤)
137, 9, 12co 7145 . . . . . . . 8 class (𝑥(+g𝑤)𝑦)
1413, 9wceq 1528 . . . . . . 7 wff (𝑥(+g𝑤)𝑦) = 𝑦
159, 7, 12co 7145 . . . . . . . 8 class (𝑦(+g𝑤)𝑥)
1615, 9wceq 1528 . . . . . . 7 wff (𝑦(+g𝑤)𝑥) = 𝑦
1714, 16wa 396 . . . . . 6 wff ((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)
18 cbs 16473 . . . . . . 7 class Base
1910, 18cfv 6349 . . . . . 6 class (Base‘𝑤)
2017, 8, 19wral 3138 . . . . 5 wff 𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)
2120, 6, 19crab 3142 . . . 4 class {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)}
223cv 1527 . . . . . . 7 class 𝑓
2322crn 5550 . . . . . 6 class ran 𝑓
245cv 1527 . . . . . 6 class 𝑜
2523, 24wss 3935 . . . . 5 wff ran 𝑓𝑜
26 c0g 16703 . . . . . 6 class 0g
2710, 26cfv 6349 . . . . 5 class (0g𝑤)
2822cdm 5549 . . . . . . 7 class dom 𝑓
29 cfz 12882 . . . . . . . 8 class ...
3029crn 5550 . . . . . . 7 class ran ...
3128, 30wcel 2105 . . . . . 6 wff dom 𝑓 ∈ ran ...
32 vm . . . . . . . . . . . . 13 setvar 𝑚
3332cv 1527 . . . . . . . . . . . 12 class 𝑚
34 vn . . . . . . . . . . . . 13 setvar 𝑛
3534cv 1527 . . . . . . . . . . . 12 class 𝑛
3633, 35, 29co 7145 . . . . . . . . . . 11 class (𝑚...𝑛)
3728, 36wceq 1528 . . . . . . . . . 10 wff dom 𝑓 = (𝑚...𝑛)
3812, 22, 33cseq 13359 . . . . . . . . . . . 12 class seq𝑚((+g𝑤), 𝑓)
3935, 38cfv 6349 . . . . . . . . . . 11 class (seq𝑚((+g𝑤), 𝑓)‘𝑛)
407, 39wceq 1528 . . . . . . . . . 10 wff 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛)
4137, 40wa 396 . . . . . . . . 9 wff (dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛))
42 cuz 12232 . . . . . . . . . 10 class
4333, 42cfv 6349 . . . . . . . . 9 class (ℤ𝑚)
4441, 34, 43wrex 3139 . . . . . . . 8 wff 𝑛 ∈ (ℤ𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛))
4544, 32wex 1771 . . . . . . 7 wff 𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛))
4645, 6cio 6306 . . . . . 6 class (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛)))
47 c1 10527 . . . . . . . . . . . 12 class 1
48 chash 13680 . . . . . . . . . . . . 13 class
499, 48cfv 6349 . . . . . . . . . . . 12 class (♯‘𝑦)
5047, 49, 29co 7145 . . . . . . . . . . 11 class (1...(♯‘𝑦))
51 vg . . . . . . . . . . . 12 setvar 𝑔
5251cv 1527 . . . . . . . . . . 11 class 𝑔
5350, 9, 52wf1o 6348 . . . . . . . . . 10 wff 𝑔:(1...(♯‘𝑦))–1-1-onto𝑦
5422, 52ccom 5553 . . . . . . . . . . . . 13 class (𝑓𝑔)
5512, 54, 47cseq 13359 . . . . . . . . . . . 12 class seq1((+g𝑤), (𝑓𝑔))
5649, 55cfv 6349 . . . . . . . . . . 11 class (seq1((+g𝑤), (𝑓𝑔))‘(♯‘𝑦))
577, 56wceq 1528 . . . . . . . . . 10 wff 𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(♯‘𝑦))
5853, 57wa 396 . . . . . . . . 9 wff (𝑔:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(♯‘𝑦)))
5922ccnv 5548 . . . . . . . . . 10 class 𝑓
604, 24cdif 3932 . . . . . . . . . 10 class (V ∖ 𝑜)
6159, 60cima 5552 . . . . . . . . 9 class (𝑓 “ (V ∖ 𝑜))
6258, 8, 61wsbc 3771 . . . . . . . 8 wff [(𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(♯‘𝑦)))
6362, 51wex 1771 . . . . . . 7 wff 𝑔[(𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(♯‘𝑦)))
6463, 6cio 6306 . . . . . 6 class (℩𝑥𝑔[(𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(♯‘𝑦))))
6531, 46, 64cif 4465 . . . . 5 class if(dom 𝑓 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛))), (℩𝑥𝑔[(𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(♯‘𝑦)))))
6625, 27, 65cif 4465 . . . 4 class if(ran 𝑓𝑜, (0g𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛))), (℩𝑥𝑔[(𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(♯‘𝑦))))))
675, 21, 66csb 3882 . . 3 class {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} / 𝑜if(ran 𝑓𝑜, (0g𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛))), (℩𝑥𝑔[(𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(♯‘𝑦))))))
682, 3, 4, 4, 67cmpo 7147 . 2 class (𝑤 ∈ V, 𝑓 ∈ V ↦ {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} / 𝑜if(ran 𝑓𝑜, (0g𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛))), (℩𝑥𝑔[(𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(♯‘𝑦)))))))
691, 68wceq 1528 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𝑤), (𝑓𝑔))‘(♯‘𝑦)))))))
Colors of variables: wff setvar class
This definition is referenced by:  gsumvalx  17876  gsum0  17884
  Copyright terms: Public domain W3C validator