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 ‘ 𝑤 ) , ( 𝑓 ∘ 𝑔 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) ) ) |