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 = ( Base ` G )
	gsumprval.p	|- .+ = ( +g ` G )
	gsumprval.g	|- ( ph -> G e. V )
	gsumprval.m	|- ( ph -> M e. ZZ )
	gsumprval.n	|- ( ph -> N = ( M + 1 ) )
	gsumprval.f	|- ( ph -> F : { M , N } --> B )
Assertion	gsumprval	|- ( ph -> ( G gsum F ) = ( ( F ` M ) .+ ( F ` N ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumprval.b	|- B = ( Base ` G )
2		gsumprval.p	|- .+ = ( +g ` G )
3		gsumprval.g	|- ( ph -> G e. V )
4		gsumprval.m	|- ( ph -> M e. ZZ )
5		gsumprval.n	|- ( ph -> N = ( M + 1 ) )
6		gsumprval.f	|- ( ph -> F : { M , N } --> B )
7		uzid	|- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
8	4 7	syl	|- ( ph -> M e. ( ZZ>= ` M ) )
9		peano2uz	|- ( M e. ( ZZ>= ` M ) -> ( M + 1 ) e. ( ZZ>= ` M ) )
10	8 9	syl	|- ( ph -> ( M + 1 ) e. ( ZZ>= ` M ) )
11		fzpr	|- ( M e. ZZ -> ( M ... ( M + 1 ) ) = { M , ( M + 1 ) } )
12	4 11	syl	|- ( ph -> ( M ... ( M + 1 ) ) = { M , ( M + 1 ) } )
13	5	eqcomd	|- ( ph -> ( M + 1 ) = N )
14	13	preq2d	|- ( ph -> { M , ( M + 1 ) } = { M , N } )
15	12 14	eqtrd	|- ( ph -> ( M ... ( M + 1 ) ) = { M , N } )
16	15	feq2d	|- ( ph -> ( F : ( M ... ( M + 1 ) ) --> B <-> F : { M , N } --> B ) )
17	6 16	mpbird	|- ( ph -> F : ( M ... ( M + 1 ) ) --> B )
18	1 2 3 10 17	gsumval2	|- ( ph -> ( G gsum F ) = ( seq M ( .+ , F ) ` ( M + 1 ) ) )
19		seqp1	|- ( M e. ( ZZ>= ` M ) -> ( seq M ( .+ , F ) ` ( M + 1 ) ) = ( ( seq M ( .+ , F ) ` M ) .+ ( F ` ( M + 1 ) ) ) )
20	8 19	syl	|- ( ph -> ( seq M ( .+ , F ) ` ( M + 1 ) ) = ( ( seq M ( .+ , F ) ` M ) .+ ( F ` ( M + 1 ) ) ) )
21		seq1	|- ( M e. ZZ -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
22	4 21	syl	|- ( ph -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
23	13	fveq2d	|- ( ph -> ( F ` ( M + 1 ) ) = ( F ` N ) )
24	22 23	oveq12d	|- ( ph -> ( ( seq M ( .+ , F ) ` M ) .+ ( F ` ( M + 1 ) ) ) = ( ( F ` M ) .+ ( F ` N ) ) )
25	18 20 24	3eqtrd	|- ( ph -> ( G gsum F ) = ( ( F ` M ) .+ ( F ` N ) ) )