Metamath Proof Explorer

Theorem gsumsplit1r

Description: Splitting off the rightmost summand of a group sum. This corresponds to the (inductive) definition of a (finite) product in Lang p. 4, first formula. (Contributed by AV, 26-Dec-2023)

Ref Expression
Hypotheses gsumsplit1r.b 
|- B = ( Base ` G )
gsumsplit1r.p 
|- .+ = ( +g ` G )
gsumsplit1r.g 
|- ( ph -> G e. V )
gsumsplit1r.m 
|- ( ph -> M e. ZZ )
gsumsplit1r.n 
|- ( ph -> N e. ( ZZ>= ` M ) )
gsumsplit1r.f 
|- ( ph -> F : ( M ... ( N + 1 ) ) --> B )
Assertion gsumsplit1r 
|- ( ph -> ( G gsum F ) = ( ( G gsum ( F |` ( M ... N ) ) ) .+ ( F ` ( N + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumsplit1r.b 
 |-  B = ( Base ` G )
2 gsumsplit1r.p 
 |-  .+ = ( +g ` G )
3 gsumsplit1r.g 
 |-  ( ph -> G e. V )
4 gsumsplit1r.m 
 |-  ( ph -> M e. ZZ )
5 gsumsplit1r.n 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
6 gsumsplit1r.f 
 |-  ( ph -> F : ( M ... ( N + 1 ) ) --> B )
7 peano2uz 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
8 5 7 syl 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )
9 1 2 3 8 6 gsumval2 
 |-  ( ph -> ( G gsum F ) = ( seq M ( .+ , F ) ` ( N + 1 ) ) )
10 seqp1 
 |-  ( N e. ( ZZ>= ` M ) -> ( seq M ( .+ , F ) ` ( N + 1 ) ) = ( ( seq M ( .+ , F ) ` N ) .+ ( F ` ( N + 1 ) ) ) )
11 5 10 syl 
 |-  ( ph -> ( seq M ( .+ , F ) ` ( N + 1 ) ) = ( ( seq M ( .+ , F ) ` N ) .+ ( F ` ( N + 1 ) ) ) )
12 fzssp1 
 |-  ( M ... N ) C_ ( M ... ( N + 1 ) )
13 12 a1i 
 |-  ( ph -> ( M ... N ) C_ ( M ... ( N + 1 ) ) )
14 6 13 fssresd 
 |-  ( ph -> ( F |` ( M ... N ) ) : ( M ... N ) --> B )
15 1 2 3 5 14 gsumval2 
 |-  ( ph -> ( G gsum ( F |` ( M ... N ) ) ) = ( seq M ( .+ , ( F |` ( M ... N ) ) ) ` N ) )
16 4 uzidd 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
17 seq1 
 |-  ( M e. ZZ -> ( seq M ( .+ , ( F |` ( M ... N ) ) ) ` M ) = ( ( F |` ( M ... N ) ) ` M ) )
18 4 17 syl 
 |-  ( ph -> ( seq M ( .+ , ( F |` ( M ... N ) ) ) ` M ) = ( ( F |` ( M ... N ) ) ` M ) )
19 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
20 5 19 syl 
 |-  ( ph -> M e. ( M ... N ) )
21 20 fvresd 
 |-  ( ph -> ( ( F |` ( M ... N ) ) ` M ) = ( F ` M ) )
22 18 21 eqtrd 
 |-  ( ph -> ( seq M ( .+ , ( F |` ( M ... N ) ) ) ` M ) = ( F ` M ) )
23 fzp1ss 
 |-  ( M e. ZZ -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
24 4 23 syl 
 |-  ( ph -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
25 24 sselda 
 |-  ( ( ph /\ x e. ( ( M + 1 ) ... N ) ) -> x e. ( M ... N ) )
26 25 fvresd 
 |-  ( ( ph /\ x e. ( ( M + 1 ) ... N ) ) -> ( ( F |` ( M ... N ) ) ` x ) = ( F ` x ) )
27 16 22 5 26 seqfveq2 
 |-  ( ph -> ( seq M ( .+ , ( F |` ( M ... N ) ) ) ` N ) = ( seq M ( .+ , F ) ` N ) )
28 15 27 eqtr2d 
 |-  ( ph -> ( seq M ( .+ , F ) ` N ) = ( G gsum ( F |` ( M ... N ) ) ) )
29 28 oveq1d 
 |-  ( ph -> ( ( seq M ( .+ , F ) ` N ) .+ ( F ` ( N + 1 ) ) ) = ( ( G gsum ( F |` ( M ... N ) ) ) .+ ( F ` ( N + 1 ) ) ) )
30 9 11 29 3eqtrd 
 |-  ( ph -> ( G gsum F ) = ( ( G gsum ( F |` ( M ... N ) ) ) .+ ( F ` ( N + 1 ) ) ) )