This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )