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

Definition df-gsum 13730
 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 three 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. etc. 3. If is a finite set (or is non-zero 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 18158. (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
Distinct variable group:   ,,,,,,,

Detailed syntax breakdown of Definition df-gsum
StepHypRef Expression
1 cgsu 13726 . 2 g
2 vw . . 3
3 vf . . 3
4 cvv 2958 . . 3
5 vo . . . 4
6 vx . . . . . . . . . 10
76cv 1652 . . . . . . . . 9
8 vy . . . . . . . . . 10
98cv 1652 . . . . . . . . 9
102cv 1652 . . . . . . . . . 10
11 cplusg 13531 . . . . . . . . . 10
1210, 11cfv 5456 . . . . . . . . 9
137, 9, 12co 6083 . . . . . . . 8
1413, 9wceq 1653 . . . . . . 7
159, 7, 12co 6083 . . . . . . . 8
1615, 9wceq 1653 . . . . . . 7
1714, 16wa 360 . . . . . 6
18 cbs 13471 . . . . . . 7
1910, 18cfv 5456 . . . . . 6
2017, 8, 19wral 2707 . . . . 5
2120, 6, 19crab 2711 . . . 4
223cv 1652 . . . . . . 7
2322crn 4881 . . . . . 6
245cv 1652 . . . . . 6
2523, 24wss 3322 . . . . 5
26 c0g 13725 . . . . . 6
2710, 26cfv 5456 . . . . 5
2822cdm 4880 . . . . . . 7
29 cfz 11045 . . . . . . . 8
3029crn 4881 . . . . . . 7
3128, 30wcel 1726 . . . . . 6
32 vm . . . . . . . . . . . . 13
3332cv 1652 . . . . . . . . . . . 12
34 vn . . . . . . . . . . . . 13
3534cv 1652 . . . . . . . . . . . 12
3633, 35, 29co 6083 . . . . . . . . . . 11
3728, 36wceq 1653 . . . . . . . . . 10
3812, 22, 33cseq 11325 . . . . . . . . . . . 12
3935, 38cfv 5456 . . . . . . . . . . 11
407, 39wceq 1653 . . . . . . . . . 10
4137, 40wa 360 . . . . . . . . 9
42 cuz 10490 . . . . . . . . . 10
4333, 42cfv 5456 . . . . . . . . 9
4441, 34, 43wrex 2708 . . . . . . . 8
4544, 32wex 1551 . . . . . . 7
4645, 6cio 5418 . . . . . 6
47 c1 8993 . . . . . . . . . . . 12
48 chash 11620 . . . . . . . . . . . . 13
499, 48cfv 5456 . . . . . . . . . . . 12
5047, 49, 29co 6083 . . . . . . . . . . 11
51 vg . . . . . . . . . . . 12
5251cv 1652 . . . . . . . . . . 11
5350, 9, 52wf1o 5455 . . . . . . . . . 10
5422, 52ccom 4884 . . . . . . . . . . . . 13
5512, 54, 47cseq 11325 . . . . . . . . . . . 12
5649, 55cfv 5456 . . . . . . . . . . 11
577, 56wceq 1653 . . . . . . . . . 10
5853, 57wa 360 . . . . . . . . 9
5922ccnv 4879 . . . . . . . . . 10
604, 24cdif 3319 . . . . . . . . . 10
6159, 60cima 4883 . . . . . . . . 9
6258, 8, 61wsbc 3163 . . . . . . . 8
6362, 51wex 1551 . . . . . . 7
6463, 6cio 5418 . . . . . 6
6531, 46, 64cif 3741 . . . . 5
6625, 27, 65cif 3741 . . . 4
675, 21, 66csb 3253 . . 3
682, 3, 4, 4, 67cmpt2 6085 . 2
691, 68wceq 1653 1 g
 Colors of variables: wff set class This definition is referenced by:  gsumvalx  14776  gsum0  14782
 Copyright terms: Public domain W3C validator