Description: Define the group sum (also called "iterated sum") for the structure G of a finite sequence of elements whose values are defined by the expression B and whose set of indices is A . It may be viewed as a product (if G is a multiplication), a sum (if G is an addition) or any other operation. The variable k is normally a free variable in B (i.e., B can be thought of as B ( k ) ). The definition is meaningful in different contexts, depending on the size of the index set A and each demanding different properties of G .
1. If A = (/) and G has an identity element, then the sum equals this identity. See gsum0 .
2. If A = ( M ... N ) and G is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e., ( B ( 1 ) + B ( 2 ) ) + B ( 3 ) , etc. See gsumval2 and gsumnunsn .
3. If A is a finite set (or is nonzero for finitely many indices) and G is a commutative monoid, then the sum adds up these elements in some order, which is then uniquely defined. See gsumval3 .
4. If A is an infinite set and G is a Hausdorff topological group, then there is a meaningful sum, but gsum cannot handle this case. See df-tsms .
Remark: this definition is required here because the symbol gsum is already used in df-prds and df-imas . The related theorems are provided later, see gsumvalx . (Contributed by FL, 5-Sep-2010) (Revised by FL, 17-Oct-2011) (Revised by Mario Carneiro, 7-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | df-gsum | ⊢ Σg = ( 𝑤 ∈ V , 𝑓 ∈ V ↦ ⦋ { 𝑥 ∈ ( Base ‘ 𝑤 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } / 𝑜 ⦌ if ( ran 𝑓 ⊆ 𝑜 , ( 0g ‘ 𝑤 ) , if ( dom 𝑓 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑓 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑓 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑔 [ ( ◡ 𝑓 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑓 ∘ 𝑔 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cgsu | ⊢ Σg | |
1 | vw | ⊢ 𝑤 | |
2 | cvv | ⊢ V | |
3 | vf | ⊢ 𝑓 | |
4 | vx | ⊢ 𝑥 | |
5 | cbs | ⊢ Base | |
6 | 1 | cv | ⊢ 𝑤 |
7 | 6 5 | cfv | ⊢ ( Base ‘ 𝑤 ) |
8 | vy | ⊢ 𝑦 | |
9 | 4 | cv | ⊢ 𝑥 |
10 | cplusg | ⊢ +g | |
11 | 6 10 | cfv | ⊢ ( +g ‘ 𝑤 ) |
12 | 8 | cv | ⊢ 𝑦 |
13 | 9 12 11 | co | ⊢ ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) |
14 | 13 12 | wceq | ⊢ ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 |
15 | 12 9 11 | co | ⊢ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) |
16 | 15 12 | wceq | ⊢ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 |
17 | 14 16 | wa | ⊢ ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) |
18 | 17 8 7 | wral | ⊢ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) |
19 | 18 4 7 | crab | ⊢ { 𝑥 ∈ ( Base ‘ 𝑤 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } |
20 | vo | ⊢ 𝑜 | |
21 | 3 | cv | ⊢ 𝑓 |
22 | 21 | crn | ⊢ ran 𝑓 |
23 | 20 | cv | ⊢ 𝑜 |
24 | 22 23 | wss | ⊢ ran 𝑓 ⊆ 𝑜 |
25 | c0g | ⊢ 0g | |
26 | 6 25 | cfv | ⊢ ( 0g ‘ 𝑤 ) |
27 | 21 | cdm | ⊢ dom 𝑓 |
28 | cfz | ⊢ ... | |
29 | 28 | crn | ⊢ ran ... |
30 | 27 29 | wcel | ⊢ dom 𝑓 ∈ ran ... |
31 | vm | ⊢ 𝑚 | |
32 | vn | ⊢ 𝑛 | |
33 | cuz | ⊢ ℤ≥ | |
34 | 31 | cv | ⊢ 𝑚 |
35 | 34 33 | cfv | ⊢ ( ℤ≥ ‘ 𝑚 ) |
36 | 32 | cv | ⊢ 𝑛 |
37 | 34 36 28 | co | ⊢ ( 𝑚 ... 𝑛 ) |
38 | 27 37 | wceq | ⊢ dom 𝑓 = ( 𝑚 ... 𝑛 ) |
39 | 11 21 34 | cseq | ⊢ seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑓 ) |
40 | 36 39 | cfv | ⊢ ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑓 ) ‘ 𝑛 ) |
41 | 9 40 | wceq | ⊢ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑓 ) ‘ 𝑛 ) |
42 | 38 41 | wa | ⊢ ( dom 𝑓 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑓 ) ‘ 𝑛 ) ) |
43 | 42 32 35 | wrex | ⊢ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑓 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑓 ) ‘ 𝑛 ) ) |
44 | 43 31 | wex | ⊢ ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑓 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑓 ) ‘ 𝑛 ) ) |
45 | 44 4 | cio | ⊢ ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑓 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑓 ) ‘ 𝑛 ) ) ) |
46 | vg | ⊢ 𝑔 | |
47 | 21 | ccnv | ⊢ ◡ 𝑓 |
48 | 2 23 | cdif | ⊢ ( V ∖ 𝑜 ) |
49 | 47 48 | cima | ⊢ ( ◡ 𝑓 “ ( V ∖ 𝑜 ) ) |
50 | 46 | cv | ⊢ 𝑔 |
51 | c1 | ⊢ 1 | |
52 | chash | ⊢ ♯ | |
53 | 12 52 | cfv | ⊢ ( ♯ ‘ 𝑦 ) |
54 | 51 53 28 | co | ⊢ ( 1 ... ( ♯ ‘ 𝑦 ) ) |
55 | 54 12 50 | wf1o | ⊢ 𝑔 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 |
56 | 21 50 | ccom | ⊢ ( 𝑓 ∘ 𝑔 ) |
57 | 11 56 51 | cseq | ⊢ seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑓 ∘ 𝑔 ) ) |
58 | 53 57 | cfv | ⊢ ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑓 ∘ 𝑔 ) ) ‘ ( ♯ ‘ 𝑦 ) ) |
59 | 9 58 | wceq | ⊢ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑓 ∘ 𝑔 ) ) ‘ ( ♯ ‘ 𝑦 ) ) |
60 | 55 59 | wa | ⊢ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑓 ∘ 𝑔 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) |
61 | 60 8 49 | wsbc | ⊢ [ ( ◡ 𝑓 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑓 ∘ 𝑔 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) |
62 | 61 46 | wex | ⊢ ∃ 𝑔 [ ( ◡ 𝑓 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑓 ∘ 𝑔 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) |
63 | 62 4 | cio | ⊢ ( ℩ 𝑥 ∃ 𝑔 [ ( ◡ 𝑓 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑓 ∘ 𝑔 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) |
64 | 30 45 63 | cif | ⊢ if ( dom 𝑓 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑓 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑓 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑔 [ ( ◡ 𝑓 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑓 ∘ 𝑔 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) |
65 | 24 26 64 | cif | ⊢ if ( ran 𝑓 ⊆ 𝑜 , ( 0g ‘ 𝑤 ) , if ( dom 𝑓 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑓 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑓 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑔 [ ( ◡ 𝑓 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑓 ∘ 𝑔 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) ) |
66 | 20 19 65 | csb | ⊢ ⦋ { 𝑥 ∈ ( Base ‘ 𝑤 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } / 𝑜 ⦌ if ( ran 𝑓 ⊆ 𝑜 , ( 0g ‘ 𝑤 ) , if ( dom 𝑓 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑓 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑓 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑔 [ ( ◡ 𝑓 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑓 ∘ 𝑔 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) ) |
67 | 1 3 2 2 66 | cmpo | ⊢ ( 𝑤 ∈ V , 𝑓 ∈ V ↦ ⦋ { 𝑥 ∈ ( Base ‘ 𝑤 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } / 𝑜 ⦌ if ( ran 𝑓 ⊆ 𝑜 , ( 0g ‘ 𝑤 ) , if ( dom 𝑓 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑓 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑓 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑔 [ ( ◡ 𝑓 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑓 ∘ 𝑔 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) ) ) |
68 | 0 67 | wceq | ⊢ Σg = ( 𝑤 ∈ V , 𝑓 ∈ V ↦ ⦋ { 𝑥 ∈ ( Base ‘ 𝑤 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } / 𝑜 ⦌ if ( ran 𝑓 ⊆ 𝑜 , ( 0g ‘ 𝑤 ) , if ( dom 𝑓 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑓 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑓 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑔 [ ( ◡ 𝑓 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑓 ∘ 𝑔 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) ) ) |