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	$$⊢{\Sigma }_{𝑔}=\left(w\in \mathrm{V},f\in \mathrm{V}⟼⦋\left\{x\in {\mathrm{Base}}_w|\forall y\in {\mathrm{Base}}_w\left(x{+}_{w}y=y\wedge y{+}_{w}x=y\right)\right\}/o⦌if\left(\mathrm{ran}f\subseteq o,0_w,if\left(\mathrm{dom}f\in \mathrm{ran}\dots ,\left(\iota x|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(\mathrm{dom}f=\left(m\dots n\right)\wedge x=seqm\left({+}_w,f\right)\left(n\right)\right)\right),\left(\iota x|\exists g\underset{\dot{}}{[}{f}^{-1}\left[\mathrm{V}\setminus o\right]/y\underset{\dot{}}{]}\left(g:\left(1\dots \left|y\right|\right)\underset{1-1\; onto}{⟶}y\wedge x=seq1\left({+}_w,\left(f\circ g\right)\right)\left(\left|y\right|\right)\right)\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgsu	$$class{\Sigma }_{𝑔}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vf	$$setvarf$$
4		vx	$$setvarx$$
5		cbs	$$class\mathrm{Base}$$
6	1	cv	$$setvarw$$
7	6 5	cfv	$$class{\mathrm{Base}}_w$$
8		vy	$$setvary$$
9	4	cv	$$setvarx$$
10		cplusg	$$class{+}_{𝑔}$$
11	6 10	cfv	$$class{+}_w$$
12	8	cv	$$setvary$$
13	9 12 11	co	$$class\left(x{+}_{w}y\right)$$
14	13 12	wceq	$$wffx{+}_{w}y=y$$
15	12 9 11	co	$$class\left(y{+}_{w}x\right)$$
16	15 12	wceq	$$wffy{+}_{w}x=y$$
17	14 16	wa	$$wff\left(x{+}_{w}y=y\wedge y{+}_{w}x=y\right)$$
18	17 8 7	wral	$$wff\forall y\in {\mathrm{Base}}_w\left(x{+}_{w}y=y\wedge y{+}_{w}x=y\right)$$
19	18 4 7	crab	$$class\left\{x\in {\mathrm{Base}}_w|\forall y\in {\mathrm{Base}}_w\left(x{+}_{w}y=y\wedge y{+}_{w}x=y\right)\right\}$$
20		vo	$$setvaro$$
21	3	cv	$$setvarf$$
22	21	crn	$$class\mathrm{ran}f$$
23	20	cv	$$setvaro$$
24	22 23	wss	$$wff\mathrm{ran}f\subseteq o$$
25		c0g	$$class{0}_{𝑔}$$
26	6 25	cfv	$$class{0}_w$$
27	21	cdm	$$class\mathrm{dom}f$$
28		cfz	$$class\dots$$
29	28	crn	$$class\mathrm{ran}\dots$$
30	27 29	wcel	$$wff\mathrm{dom}f\in \mathrm{ran}\dots$$
31		vm	$$setvarm$$
32		vn	$$setvarn$$
33		cuz	$$class{\mathbb{Z}}_{\ge }$$
34	31	cv	$$setvarm$$
35	34 33	cfv	$$class{\mathbb{Z}}_{\ge m}$$
36	32	cv	$$setvarn$$
37	34 36 28	co	$$class\left(m\dots n\right)$$
38	27 37	wceq	$$wff\mathrm{dom}f=\left(m\dots n\right)$$
39	11 21 34	cseq	$$classseqm\left({+}_w,f\right)$$
40	36 39	cfv	$$classseqm\left({+}_w,f\right)\left(n\right)$$
41	9 40	wceq	$$wffx=seqm\left({+}_w,f\right)\left(n\right)$$
42	38 41	wa	$$wff\left(\mathrm{dom}f=\left(m\dots n\right)\wedge x=seqm\left({+}_w,f\right)\left(n\right)\right)$$
43	42 32 35	wrex	$$wff\exists n\in {\mathbb{Z}}_{\ge m}\left(\mathrm{dom}f=\left(m\dots n\right)\wedge x=seqm\left({+}_w,f\right)\left(n\right)\right)$$
44	43 31	wex	$$wff\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(\mathrm{dom}f=\left(m\dots n\right)\wedge x=seqm\left({+}_w,f\right)\left(n\right)\right)$$
45	44 4	cio	$$class\left(\iota x|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(\mathrm{dom}f=\left(m\dots n\right)\wedge x=seqm\left({+}_w,f\right)\left(n\right)\right)\right)$$
46		vg	$$setvarg$$
47	21	ccnv	$$class{f}^{-1}$$
48	2 23	cdif	$$class\left(\mathrm{V}\setminus o\right)$$
49	47 48	cima	$$class{f}^{-1}\left[\mathrm{V}\setminus o\right]$$
50	46	cv	$$setvarg$$
51		c1	$$class1$$
52		chash	$$class\left|.\right|$$
53	12 52	cfv	$$class\left|y\right|$$
54	51 53 28	co	$$class\left(1\dots \left|y\right|\right)$$
55	54 12 50	wf1o	$$wffg:\left(1\dots \left|y\right|\right)\underset{1-1\; onto}{⟶}y$$
56	21 50	ccom	$$class\left(f\circ g\right)$$
57	11 56 51	cseq	$$classseq1\left({+}_w,\left(f\circ g\right)\right)$$
58	53 57	cfv	$$classseq1\left({+}_w,\left(f\circ g\right)\right)\left(\left|y\right|\right)$$
59	9 58	wceq	$$wffx=seq1\left({+}_w,\left(f\circ g\right)\right)\left(\left|y\right|\right)$$
60	55 59	wa	$$wff\left(g:\left(1\dots \left|y\right|\right)\underset{1-1\; onto}{⟶}y\wedge x=seq1\left({+}_w,\left(f\circ g\right)\right)\left(\left|y\right|\right)\right)$$
61	60 8 49	wsbc	$$wff\underset{\dot{}}{[}{f}^{-1}\left[\mathrm{V}\setminus o\right]/y\underset{\dot{}}{]}\left(g:\left(1\dots \left|y\right|\right)\underset{1-1\; onto}{⟶}y\wedge x=seq1\left({+}_w,\left(f\circ g\right)\right)\left(\left|y\right|\right)\right)$$
62	61 46	wex	$$wff\exists g\underset{\dot{}}{[}{f}^{-1}\left[\mathrm{V}\setminus o\right]/y\underset{\dot{}}{]}\left(g:\left(1\dots \left|y\right|\right)\underset{1-1\; onto}{⟶}y\wedge x=seq1\left({+}_w,\left(f\circ g\right)\right)\left(\left|y\right|\right)\right)$$
63	62 4	cio	$$class\left(\iota x|\exists g\underset{\dot{}}{[}{f}^{-1}\left[\mathrm{V}\setminus o\right]/y\underset{\dot{}}{]}\left(g:\left(1\dots \left|y\right|\right)\underset{1-1\; onto}{⟶}y\wedge x=seq1\left({+}_w,\left(f\circ g\right)\right)\left(\left|y\right|\right)\right)\right)$$
64	30 45 63	cif	$$classif\left(\mathrm{dom}f\in \mathrm{ran}\dots ,\left(\iota x|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(\mathrm{dom}f=\left(m\dots n\right)\wedge x=seqm\left({+}_w,f\right)\left(n\right)\right)\right),\left(\iota x|\exists g\underset{\dot{}}{[}{f}^{-1}\left[\mathrm{V}\setminus o\right]/y\underset{\dot{}}{]}\left(g:\left(1\dots \left|y\right|\right)\underset{1-1\; onto}{⟶}y\wedge x=seq1\left({+}_w,\left(f\circ g\right)\right)\left(\left|y\right|\right)\right)\right)\right)$$
65	24 26 64	cif	$$classif\left(\mathrm{ran}f\subseteq o,0_w,if\left(\mathrm{dom}f\in \mathrm{ran}\dots ,\left(\iota x|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(\mathrm{dom}f=\left(m\dots n\right)\wedge x=seqm\left({+}_w,f\right)\left(n\right)\right)\right),\left(\iota x|\exists g\underset{\dot{}}{[}{f}^{-1}\left[\mathrm{V}\setminus o\right]/y\underset{\dot{}}{]}\left(g:\left(1\dots \left|y\right|\right)\underset{1-1\; onto}{⟶}y\wedge x=seq1\left({+}_w,\left(f\circ g\right)\right)\left(\left|y\right|\right)\right)\right)\right)\right)$$
66	20 19 65	csb	$$class⦋\left\{x\in {\mathrm{Base}}_w|\forall y\in {\mathrm{Base}}_w\left(x{+}_{w}y=y\wedge y{+}_{w}x=y\right)\right\}/o⦌if\left(\mathrm{ran}f\subseteq o,0_w,if\left(\mathrm{dom}f\in \mathrm{ran}\dots ,\left(\iota x|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(\mathrm{dom}f=\left(m\dots n\right)\wedge x=seqm\left({+}_w,f\right)\left(n\right)\right)\right),\left(\iota x|\exists g\underset{\dot{}}{[}{f}^{-1}\left[\mathrm{V}\setminus o\right]/y\underset{\dot{}}{]}\left(g:\left(1\dots \left|y\right|\right)\underset{1-1\; onto}{⟶}y\wedge x=seq1\left({+}_w,\left(f\circ g\right)\right)\left(\left|y\right|\right)\right)\right)\right)\right)$$
67	1 3 2 2 66	cmpo	$$class\left(w\in \mathrm{V},f\in \mathrm{V}⟼⦋\left\{x\in {\mathrm{Base}}_w|\forall y\in {\mathrm{Base}}_w\left(x{+}_{w}y=y\wedge y{+}_{w}x=y\right)\right\}/o⦌if\left(\mathrm{ran}f\subseteq o,0_w,if\left(\mathrm{dom}f\in \mathrm{ran}\dots ,\left(\iota x|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(\mathrm{dom}f=\left(m\dots n\right)\wedge x=seqm\left({+}_w,f\right)\left(n\right)\right)\right),\left(\iota x|\exists g\underset{\dot{}}{[}{f}^{-1}\left[\mathrm{V}\setminus o\right]/y\underset{\dot{}}{]}\left(g:\left(1\dots \left|y\right|\right)\underset{1-1\; onto}{⟶}y\wedge x=seq1\left({+}_w,\left(f\circ g\right)\right)\left(\left|y\right|\right)\right)\right)\right)\right)\right)$$
68	0 67	wceq	$$wff{\Sigma }_{𝑔}=\left(w\in \mathrm{V},f\in \mathrm{V}⟼⦋\left\{x\in {\mathrm{Base}}_w|\forall y\in {\mathrm{Base}}_w\left(x{+}_{w}y=y\wedge y{+}_{w}x=y\right)\right\}/o⦌if\left(\mathrm{ran}f\subseteq o,0_w,if\left(\mathrm{dom}f\in \mathrm{ran}\dots ,\left(\iota x|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(\mathrm{dom}f=\left(m\dots n\right)\wedge x=seqm\left({+}_w,f\right)\left(n\right)\right)\right),\left(\iota x|\exists g\underset{\dot{}}{[}{f}^{-1}\left[\mathrm{V}\setminus o\right]/y\underset{\dot{}}{]}\left(g:\left(1\dots \left|y\right|\right)\underset{1-1\; onto}{⟶}y\wedge x=seq1\left({+}_w,\left(f\circ g\right)\right)\left(\left|y\right|\right)\right)\right)\right)\right)\right)$$