Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-gsum Unicode version

Definition df-gsum 11983
 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 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. 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 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. (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 11981 . 2 g
2 vw . . 3
3 vf . . 3
4 cvv 2657 . . 3
5 vo . . . 4
6 vx . . . . . . . . . 10
76cv 1313 . . . . . . . . 9
8 vy . . . . . . . . . 10
98cv 1313 . . . . . . . . 9
102cv 1313 . . . . . . . . . 10
11 cplusg 11864 . . . . . . . . . 10
1210, 11cfv 5081 . . . . . . . . 9
137, 9, 12co 5728 . . . . . . . 8
1413, 9wceq 1314 . . . . . . 7
159, 7, 12co 5728 . . . . . . . 8
1615, 9wceq 1314 . . . . . . 7
1714, 16wa 103 . . . . . 6
18 cbs 11802 . . . . . . 7
1910, 18cfv 5081 . . . . . 6
2017, 8, 19wral 2390 . . . . 5
2120, 6, 19crab 2394 . . . 4
223cv 1313 . . . . . . 7
2322crn 4500 . . . . . 6
245cv 1313 . . . . . 6
2523, 24wss 3037 . . . . 5
26 c0g 11980 . . . . . 6
2710, 26cfv 5081 . . . . 5
2822cdm 4499 . . . . . . 7
29 cfz 9683 . . . . . . . 8
3029crn 4500 . . . . . . 7
3128, 30wcel 1463 . . . . . 6
32 vm . . . . . . . . . . . . 13
3332cv 1313 . . . . . . . . . . . 12
34 vn . . . . . . . . . . . . 13
3534cv 1313 . . . . . . . . . . . 12
3633, 35, 29co 5728 . . . . . . . . . . 11
3728, 36wceq 1314 . . . . . . . . . 10
3812, 22, 33cseq 10111 . . . . . . . . . . . 12
3935, 38cfv 5081 . . . . . . . . . . 11
407, 39wceq 1314 . . . . . . . . . 10
4137, 40wa 103 . . . . . . . . 9
42 cuz 9228 . . . . . . . . . 10
4333, 42cfv 5081 . . . . . . . . 9
4441, 34, 43wrex 2391 . . . . . . . 8
4544, 32wex 1451 . . . . . . 7
4645, 6cio 5044 . . . . . 6
47 c1 7548 . . . . . . . . . . . 12
48 chash 10414 . . . . . . . . . . . . 13
499, 48cfv 5081 . . . . . . . . . . . 12
5047, 49, 29co 5728 . . . . . . . . . . 11
51 vg . . . . . . . . . . . 12
5251cv 1313 . . . . . . . . . . 11
5350, 9, 52wf1o 5080 . . . . . . . . . 10
5422, 52ccom 4503 . . . . . . . . . . . . 13
5512, 54, 47cseq 10111 . . . . . . . . . . . 12
5649, 55cfv 5081 . . . . . . . . . . 11
577, 56wceq 1314 . . . . . . . . . 10
5853, 57wa 103 . . . . . . . . 9
5922ccnv 4498 . . . . . . . . . 10
604, 24cdif 3034 . . . . . . . . . 10
6159, 60cima 4502 . . . . . . . . 9
6258, 8, 61wsbc 2878 . . . . . . . 8
6362, 51wex 1451 . . . . . . 7
6463, 6cio 5044 . . . . . 6
6531, 46, 64cif 3440 . . . . 5
6625, 27, 65cif 3440 . . . 4
675, 21, 66csb 2971 . . 3
682, 3, 4, 4, 67cmpo 5730 . 2
691, 68wceq 1314 1 g
 Colors of variables: wff set class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator