Theorem gsumval2

Description: Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014)

	Ref	Expression
Hypotheses	gsumval2.b	$$⊢B={\mathrm{Base}}_G$$
	gsumval2.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumval2.g	$$⊢\phi \to G\in V$$
	gsumval2.n	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
	gsumval2.f	$$⊢\phi \to F:\left(M\dots N\right)⟶B$$
Assertion	gsumval2	$$⊢\phi \to {\sum }_{G}F=seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsumval2.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumval2.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		gsumval2.g	$$⊢\phi \to G\in V$$
4		gsumval2.n	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
5		gsumval2.f	$$⊢\phi \to F:\left(M\dots N\right)⟶B$$
6		eqid	$$⊢0_G=0_G$$
7		eqid	$$⊢\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}=\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}$$
8	3	adantr	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to G\in V$$
9		ovexd	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to \left(M\dots N\right)\in \mathrm{V}$$
10	5	ffnd	$$⊢\phi \to FFn\left(M\dots N\right)$$
11	10	adantr	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to FFn\left(M\dots N\right)$$
12		simpr	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}$$
13		df-f	$$⊢F:\left(M\dots N\right)⟶\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\leftrightarrow \left(FFn\left(M\dots N\right)\wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)$$
14	11 12 13	sylanbrc	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to F:\left(M\dots N\right)⟶\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}$$
15	1 6 2 7 8 9 14	gsumval1	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to {\sum }_{G}F=0_G$$
16		simpl	$$⊢\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\to x\underset{\dot{}}{+}y=y$$
17	16	ralimi	$$⊢\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\to \forall y\in Bx\underset{\dot{}}{+}y=y$$
18	17	a1i	$$⊢x\in B\to \left(\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\to \forall y\in Bx\underset{\dot{}}{+}y=y\right)$$
19	18	ss2rabi	$$⊢\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\subseteq \left\{x\in B|\forall y\in Bx\underset{\dot{}}{+}y=y\right\}$$
20		fvex	$$⊢0_G\in \mathrm{V}$$
21	20	snid	$$⊢0_G\in \left\{0_G\right\}$$
22	5	fdmd	$$⊢\phi \to \mathrm{dom}F=\left(M\dots N\right)$$
23		eluzfz1	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \left(M\dots N\right)$$
24		ne0i	$$⊢M\in \left(M\dots N\right)\to \left(M\dots N\right)\ne \varnothing$$
25	4 23 24	3syl	$$⊢\phi \to \left(M\dots N\right)\ne \varnothing$$
26	22 25	eqnetrd	$$⊢\phi \to \mathrm{dom}F\ne \varnothing$$
27		dm0rn0	$$⊢\mathrm{dom}F=\varnothing \leftrightarrow \mathrm{ran}F=\varnothing$$
28	27	necon3bii	$$⊢\mathrm{dom}F\ne \varnothing \leftrightarrow \mathrm{ran}F\ne \varnothing$$
29	26 28	sylib	$$⊢\phi \to \mathrm{ran}F\ne \varnothing$$
30	29	adantr	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to \mathrm{ran}F\ne \varnothing$$
31		ssn0	$$⊢\left(\mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\wedge \mathrm{ran}F\ne \varnothing \right)\to \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\ne \varnothing$$
32	12 30 31	syl2anc	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\ne \varnothing$$
33	32	neneqd	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to \neg \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}=\varnothing$$
34	1 6 2 7	mgmidsssn0	$$⊢G\in V\to \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\subseteq \left\{0_G\right\}$$
35	3 34	syl	$$⊢\phi \to \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\subseteq \left\{0_G\right\}$$
36		sssn	$$⊢\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\subseteq \left\{0_G\right\}\leftrightarrow \left(\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}=\varnothing \vee \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}=\left\{0_G\right\}\right)$$
37	35 36	sylib	$$⊢\phi \to \left(\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}=\varnothing \vee \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}=\left\{0_G\right\}\right)$$
38	37	orcanai	$$⊢\left(\phi \wedge \neg \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}=\varnothing \right)\to \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}=\left\{0_G\right\}$$
39	33 38	syldan	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}=\left\{0_G\right\}$$
40	21 39	eleqtrrid	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to 0_G\in \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}$$
41	19 40	sseldi	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to 0_G\in \left\{x\in B|\forall y\in Bx\underset{\dot{}}{+}y=y\right\}$$
42		oveq1	$$⊢x=0_G\to x\underset{\dot{}}{+}y=0_G\underset{\dot{}}{+}y$$
43	42	eqeq1d	$$⊢x=0_G\to \left(x\underset{\dot{}}{+}y=y\leftrightarrow 0_G\underset{\dot{}}{+}y=y\right)$$
44	43	ralbidv	$$⊢x=0_G\to \left(\forall y\in Bx\underset{\dot{}}{+}y=y\leftrightarrow \forall y\in B{0}_G\underset{\dot{}}{+}y=y\right)$$
45	44	elrab	$$⊢0_G\in \left\{x\in B|\forall y\in Bx\underset{\dot{}}{+}y=y\right\}\leftrightarrow \left(0_G\in B\wedge \forall y\in B{0}_G\underset{\dot{}}{+}y=y\right)$$
46		oveq2	$$⊢y=0_G\to 0_G\underset{\dot{}}{+}y=0_G\underset{\dot{}}{+}{0}_G$$
47		id	$$⊢y=0_G\to y=0_G$$
48	46 47	eqeq12d	$$⊢y=0_G\to \left(0_G\underset{\dot{}}{+}y=y\leftrightarrow 0_G\underset{\dot{}}{+}{0}_G=0_G\right)$$
49	48	rspcva	$$⊢\left(0_G\in B\wedge \forall y\in B{0}_G\underset{\dot{}}{+}y=y\right)\to 0_G\underset{\dot{}}{+}{0}_G=0_G$$
50	45 49	sylbi	$$⊢0_G\in \left\{x\in B|\forall y\in Bx\underset{\dot{}}{+}y=y\right\}\to 0_G\underset{\dot{}}{+}{0}_G=0_G$$
51	41 50	syl	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to 0_G\underset{\dot{}}{+}{0}_G=0_G$$
52	4	adantr	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to N\in {\mathbb{Z}}_{\ge M}$$
53	35	ad2antrr	$$⊢\left(\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\wedge z\in \left(M\dots N\right)\right)\to \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\subseteq \left\{0_G\right\}$$
54	14	ffvelrnda	$$⊢\left(\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\wedge z\in \left(M\dots N\right)\right)\to F\left(z\right)\in \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}$$
55	53 54	sseldd	$$⊢\left(\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\wedge z\in \left(M\dots N\right)\right)\to F\left(z\right)\in \left\{0_G\right\}$$
56		elsni	$$⊢F\left(z\right)\in \left\{0_G\right\}\to F\left(z\right)=0_G$$
57	55 56	syl	$$⊢\left(\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\wedge z\in \left(M\dots N\right)\right)\to F\left(z\right)=0_G$$
58	51 52 57	seqid3	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)=0_G$$
59	15 58	eqtr4d	$$⊢\left(\phi \wedge \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to {\sum }_{G}F=seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)$$
60	3	adantr	$$⊢\left(\phi \wedge \neg \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to G\in V$$
61	4	adantr	$$⊢\left(\phi \wedge \neg \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to N\in {\mathbb{Z}}_{\ge M}$$
62	5	adantr	$$⊢\left(\phi \wedge \neg \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to F:\left(M\dots N\right)⟶B$$
63		simpr	$$⊢\left(\phi \wedge \neg \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to \neg \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}$$
64	1 2 60 61 62 7 63	gsumval2a	$$⊢\left(\phi \wedge \neg \mathrm{ran}F\subseteq \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\right)\to {\sum }_{G}F=seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)$$
65	59 64	pm2.61dan	$$⊢\phi \to {\sum }_{G}F=seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)$$