Theorem gsumprval

Description: Value of the group sum operation over a pair of sequential integers. (Contributed by AV, 14-Dec-2018)

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

Proof

Step	Hyp	Ref	Expression
1		gsumprval.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumprval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		gsumprval.g	$$⊢\phi \to G\in V$$
4		gsumprval.m	$$⊢\phi \to M\in \mathbb{Z}$$
5		gsumprval.n	$$⊢\phi \to N=M+1$$
6		gsumprval.f	$$⊢\phi \to F:\left\{M,N\right\}⟶B$$
7		uzid	$$⊢M\in \mathbb{Z}\to M\in {\mathbb{Z}}_{\ge M}$$
8	4 7	syl	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge M}$$
9		peano2uz	$$⊢M\in {\mathbb{Z}}_{\ge M}\to M+1\in {\mathbb{Z}}_{\ge M}$$
10	8 9	syl	$$⊢\phi \to M+1\in {\mathbb{Z}}_{\ge M}$$
11		fzpr	$$⊢M\in \mathbb{Z}\to \left(M\dots M+1\right)=\left\{M,M+1\right\}$$
12	4 11	syl	$$⊢\phi \to \left(M\dots M+1\right)=\left\{M,M+1\right\}$$
13	5	eqcomd	$$⊢\phi \to M+1=N$$
14	13	preq2d	$$⊢\phi \to \left\{M,M+1\right\}=\left\{M,N\right\}$$
15	12 14	eqtrd	$$⊢\phi \to \left(M\dots M+1\right)=\left\{M,N\right\}$$
16	15	feq2d	$$⊢\phi \to \left(F:\left(M\dots M+1\right)⟶B\leftrightarrow F:\left\{M,N\right\}⟶B\right)$$
17	6 16	mpbird	$$⊢\phi \to F:\left(M\dots M+1\right)⟶B$$
18	1 2 3 10 17	gsumval2	$$⊢\phi \to {\sum }_{G}F=seqM\left(\underset{\dot{}}{+},F\right)\left(M+1\right)$$
19		seqp1	$$⊢M\in {\mathbb{Z}}_{\ge M}\to seqM\left(\underset{\dot{}}{+},F\right)\left(M+1\right)=seqM\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}F\left(M+1\right)$$
20	8 19	syl	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(M+1\right)=seqM\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}F\left(M+1\right)$$
21		seq1	$$⊢M\in \mathbb{Z}\to seqM\left(\underset{\dot{}}{+},F\right)\left(M\right)=F\left(M\right)$$
22	4 21	syl	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(M\right)=F\left(M\right)$$
23	13	fveq2d	$$⊢\phi \to F\left(M+1\right)=F\left(N\right)$$
24	22 23	oveq12d	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}F\left(M+1\right)=F\left(M\right)\underset{\dot{}}{+}F\left(N\right)$$
25	18 20 24	3eqtrd	$$⊢\phi \to {\sum }_{G}F=F\left(M\right)\underset{\dot{}}{+}F\left(N\right)$$