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 15926
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 21740. Remark: this definition is required here because the symbol Σg is already used in df-prds 15931 and df-imas 15991. The related theorems are provided later, see gsumvalx 17093. (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 15924 . 2 class Σg
2 vw . . 3 setvar 𝑤
3 vf . . 3 setvar 𝑓
4 cvv 3173 . . 3 class V
5 vo . . . 4 setvar 𝑜
6 vx . . . . . . . . . 10 setvar 𝑥
76cv 1474 . . . . . . . . 9 class 𝑥
8 vy . . . . . . . . . 10 setvar 𝑦
98cv 1474 . . . . . . . . 9 class 𝑦
102cv 1474 . . . . . . . . . 10 class 𝑤
11 cplusg 15768 . . . . . . . . . 10 class +g
1210, 11cfv 5804 . . . . . . . . 9 class (+g𝑤)
137, 9, 12co 6549 . . . . . . . 8 class (𝑥(+g𝑤)𝑦)
1413, 9wceq 1475 . . . . . . 7 wff (𝑥(+g𝑤)𝑦) = 𝑦
159, 7, 12co 6549 . . . . . . . 8 class (𝑦(+g𝑤)𝑥)
1615, 9wceq 1475 . . . . . . 7 wff (𝑦(+g𝑤)𝑥) = 𝑦
1714, 16wa 383 . . . . . 6 wff ((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)
18 cbs 15695 . . . . . . 7 class Base
1910, 18cfv 5804 . . . . . 6 class (Base‘𝑤)
2017, 8, 19wral 2896 . . . . 5 wff 𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)
2120, 6, 19crab 2900 . . . 4 class {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)}
223cv 1474 . . . . . . 7 class 𝑓
2322crn 5039 . . . . . 6 class ran 𝑓
245cv 1474 . . . . . 6 class 𝑜
2523, 24wss 3540 . . . . 5 wff ran 𝑓𝑜
26 c0g 15923 . . . . . 6 class 0g
2710, 26cfv 5804 . . . . 5 class (0g𝑤)
2822cdm 5038 . . . . . . 7 class dom 𝑓
29 cfz 12197 . . . . . . . 8 class ...
3029crn 5039 . . . . . . 7 class ran ...
3128, 30wcel 1977 . . . . . 6 wff dom 𝑓 ∈ ran ...
32 vm . . . . . . . . . . . . 13 setvar 𝑚
3332cv 1474 . . . . . . . . . . . 12 class 𝑚
34 vn . . . . . . . . . . . . 13 setvar 𝑛
3534cv 1474 . . . . . . . . . . . 12 class 𝑛
3633, 35, 29co 6549 . . . . . . . . . . 11 class (𝑚...𝑛)
3728, 36wceq 1475 . . . . . . . . . 10 wff dom 𝑓 = (𝑚...𝑛)
3812, 22, 33cseq 12663 . . . . . . . . . . . 12 class seq𝑚((+g𝑤), 𝑓)
3935, 38cfv 5804 . . . . . . . . . . 11 class (seq𝑚((+g𝑤), 𝑓)‘𝑛)
407, 39wceq 1475 . . . . . . . . . 10 wff 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛)
4137, 40wa 383 . . . . . . . . 9 wff (dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛))
42 cuz 11563 . . . . . . . . . 10 class
4333, 42cfv 5804 . . . . . . . . 9 class (ℤ𝑚)
4441, 34, 43wrex 2897 . . . . . . . 8 wff 𝑛 ∈ (ℤ𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛))
4544, 32wex 1695 . . . . . . 7 wff 𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛))
4645, 6cio 5766 . . . . . 6 class (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛)))
47 c1 9816 . . . . . . . . . . . 12 class 1
48 chash 12979 . . . . . . . . . . . . 13 class #
499, 48cfv 5804 . . . . . . . . . . . 12 class (#‘𝑦)
5047, 49, 29co 6549 . . . . . . . . . . 11 class (1...(#‘𝑦))
51 vg . . . . . . . . . . . 12 setvar 𝑔
5251cv 1474 . . . . . . . . . . 11 class 𝑔
5350, 9, 52wf1o 5803 . . . . . . . . . 10 wff 𝑔:(1...(#‘𝑦))–1-1-onto𝑦
5422, 52ccom 5042 . . . . . . . . . . . . 13 class (𝑓𝑔)
5512, 54, 47cseq 12663 . . . . . . . . . . . 12 class seq1((+g𝑤), (𝑓𝑔))
5649, 55cfv 5804 . . . . . . . . . . 11 class (seq1((+g𝑤), (𝑓𝑔))‘(#‘𝑦))
577, 56wceq 1475 . . . . . . . . . 10 wff 𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(#‘𝑦))
5853, 57wa 383 . . . . . . . . 9 wff (𝑔:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(#‘𝑦)))
5922ccnv 5037 . . . . . . . . . 10 class 𝑓
604, 24cdif 3537 . . . . . . . . . 10 class (V ∖ 𝑜)
6159, 60cima 5041 . . . . . . . . 9 class (𝑓 “ (V ∖ 𝑜))
6258, 8, 61wsbc 3402 . . . . . . . 8 wff [(𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(#‘𝑦)))
6362, 51wex 1695 . . . . . . 7 wff 𝑔[(𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(#‘𝑦)))
6463, 6cio 5766 . . . . . 6 class (℩𝑥𝑔[(𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(#‘𝑦))))
6531, 46, 64cif 4036 . . . . 5 class if(dom 𝑓 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛))), (℩𝑥𝑔[(𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(#‘𝑦)))))
6625, 27, 65cif 4036 . . . 4 class if(ran 𝑓𝑜, (0g𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑓)‘𝑛))), (℩𝑥𝑔[(𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑓𝑔))‘(#‘𝑦))))))
675, 21, 66csb 3499 . . 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, 67cmpt2 6551 . 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 1475 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  17093  gsum0  17101
  Copyright terms: Public domain W3C validator