Metamath Proof Explorer


Definition df-gsum

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

Detailed syntax breakdown

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