Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-gsum | Unicode version |
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.) |
Ref | Expression |
---|---|
df-gsum | g ♯ ♯ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cgsu 12138 | . 2 g | |
2 | vw | . . 3 | |
3 | vf | . . 3 | |
4 | cvv 2686 | . . 3 | |
5 | vo | . . . 4 | |
6 | vx | . . . . . . . . . 10 | |
7 | 6 | cv 1330 | . . . . . . . . 9 |
8 | vy | . . . . . . . . . 10 | |
9 | 8 | cv 1330 | . . . . . . . . 9 |
10 | 2 | cv 1330 | . . . . . . . . . 10 |
11 | cplusg 12021 | . . . . . . . . . 10 | |
12 | 10, 11 | cfv 5123 | . . . . . . . . 9 |
13 | 7, 9, 12 | co 5774 | . . . . . . . 8 |
14 | 13, 9 | wceq 1331 | . . . . . . 7 |
15 | 9, 7, 12 | co 5774 | . . . . . . . 8 |
16 | 15, 9 | wceq 1331 | . . . . . . 7 |
17 | 14, 16 | wa 103 | . . . . . 6 |
18 | cbs 11959 | . . . . . . 7 | |
19 | 10, 18 | cfv 5123 | . . . . . 6 |
20 | 17, 8, 19 | wral 2416 | . . . . 5 |
21 | 20, 6, 19 | crab 2420 | . . . 4 |
22 | 3 | cv 1330 | . . . . . . 7 |
23 | 22 | crn 4540 | . . . . . 6 |
24 | 5 | cv 1330 | . . . . . 6 |
25 | 23, 24 | wss 3071 | . . . . 5 |
26 | c0g 12137 | . . . . . 6 | |
27 | 10, 26 | cfv 5123 | . . . . 5 |
28 | 22 | cdm 4539 | . . . . . . 7 |
29 | cfz 9790 | . . . . . . . 8 | |
30 | 29 | crn 4540 | . . . . . . 7 |
31 | 28, 30 | wcel 1480 | . . . . . 6 |
32 | vm | . . . . . . . . . . . . 13 | |
33 | 32 | cv 1330 | . . . . . . . . . . . 12 |
34 | vn | . . . . . . . . . . . . 13 | |
35 | 34 | cv 1330 | . . . . . . . . . . . 12 |
36 | 33, 35, 29 | co 5774 | . . . . . . . . . . 11 |
37 | 28, 36 | wceq 1331 | . . . . . . . . . 10 |
38 | 12, 22, 33 | cseq 10218 | . . . . . . . . . . . 12 |
39 | 35, 38 | cfv 5123 | . . . . . . . . . . 11 |
40 | 7, 39 | wceq 1331 | . . . . . . . . . 10 |
41 | 37, 40 | wa 103 | . . . . . . . . 9 |
42 | cuz 9326 | . . . . . . . . . 10 | |
43 | 33, 42 | cfv 5123 | . . . . . . . . 9 |
44 | 41, 34, 43 | wrex 2417 | . . . . . . . 8 |
45 | 44, 32 | wex 1468 | . . . . . . 7 |
46 | 45, 6 | cio 5086 | . . . . . 6 |
47 | c1 7621 | . . . . . . . . . . . 12 | |
48 | chash 10521 | . . . . . . . . . . . . 13 ♯ | |
49 | 9, 48 | cfv 5123 | . . . . . . . . . . . 12 ♯ |
50 | 47, 49, 29 | co 5774 | . . . . . . . . . . 11 ♯ |
51 | vg | . . . . . . . . . . . 12 | |
52 | 51 | cv 1330 | . . . . . . . . . . 11 |
53 | 50, 9, 52 | wf1o 5122 | . . . . . . . . . 10 ♯ |
54 | 22, 52 | ccom 4543 | . . . . . . . . . . . . 13 |
55 | 12, 54, 47 | cseq 10218 | . . . . . . . . . . . 12 |
56 | 49, 55 | cfv 5123 | . . . . . . . . . . 11 ♯ |
57 | 7, 56 | wceq 1331 | . . . . . . . . . 10 ♯ |
58 | 53, 57 | wa 103 | . . . . . . . . 9 ♯ ♯ |
59 | 22 | ccnv 4538 | . . . . . . . . . 10 |
60 | 4, 24 | cdif 3068 | . . . . . . . . . 10 |
61 | 59, 60 | cima 4542 | . . . . . . . . 9 |
62 | 58, 8, 61 | wsbc 2909 | . . . . . . . 8 ♯ ♯ |
63 | 62, 51 | wex 1468 | . . . . . . 7 ♯ ♯ |
64 | 63, 6 | cio 5086 | . . . . . 6 ♯ ♯ |
65 | 31, 46, 64 | cif 3474 | . . . . 5 ♯ ♯ |
66 | 25, 27, 65 | cif 3474 | . . . 4 ♯ ♯ |
67 | 5, 21, 66 | csb 3003 | . . 3 ♯ ♯ |
68 | 2, 3, 4, 4, 67 | cmpo 5776 | . 2 ♯ ♯ |
69 | 1, 68 | wceq 1331 | 1 g ♯ ♯ |
Colors of variables: wff set class |
This definition is referenced by: (None) |
Copyright terms: Public domain | W3C validator |