Metamath Proof Explorer

Theorem telgsumfz

Description: Telescoping group sum ranging over a finite set of sequential integers, using implicit substitution, analogous to telfsum . (Contributed by AV, 23-Nov-2019)

Ref Expression
Hypotheses telgsumfz.b 
|- B = ( Base ` G )
telgsumfz.g 
|- ( ph -> G e. Abel )
telgsumfz.m 
|- .- = ( -g ` G )
telgsumfz.n 
|- ( ph -> N e. ( ZZ>= ` M ) )
telgsumfz.f 
|- ( ph -> A. k e. ( M ... ( N + 1 ) ) A e. B )
telgsumfz.l 
|- ( k = i -> A = L )
telgsumfz.c 
|- ( k = ( i + 1 ) -> A = C )
telgsumfz.d 
|- ( k = M -> A = D )
telgsumfz.e 
|- ( k = ( N + 1 ) -> A = E )
Assertion telgsumfz 
|- ( ph -> ( G gsum ( i e. ( M ... N ) |-> ( L .- C ) ) ) = ( D .- E ) )

Proof

Step Hyp Ref Expression
1 telgsumfz.b 
 |-  B = ( Base ` G )
2 telgsumfz.g 
 |-  ( ph -> G e. Abel )
3 telgsumfz.m 
 |-  .- = ( -g ` G )
4 telgsumfz.n 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
5 telgsumfz.f 
 |-  ( ph -> A. k e. ( M ... ( N + 1 ) ) A e. B )
6 telgsumfz.l 
 |-  ( k = i -> A = L )
7 telgsumfz.c 
 |-  ( k = ( i + 1 ) -> A = C )
8 telgsumfz.d 
 |-  ( k = M -> A = D )
9 telgsumfz.e 
 |-  ( k = ( N + 1 ) -> A = E )
10 simpr 
 |-  ( ( ph /\ i e. ( M ... N ) ) -> i e. ( M ... N ) )
11 6 adantl 
 |-  ( ( ( ph /\ i e. ( M ... N ) ) /\ k = i ) -> A = L )
12 10 11 csbied 
 |-  ( ( ph /\ i e. ( M ... N ) ) -> [_ i / k ]_ A = L )
13 12 eqcomd 
 |-  ( ( ph /\ i e. ( M ... N ) ) -> L = [_ i / k ]_ A )
14 ovexd 
 |-  ( ( ph /\ i e. ( M ... N ) ) -> ( i + 1 ) e. _V )
15 7 adantl 
 |-  ( ( ( ph /\ i e. ( M ... N ) ) /\ k = ( i + 1 ) ) -> A = C )
16 14 15 csbied 
 |-  ( ( ph /\ i e. ( M ... N ) ) -> [_ ( i + 1 ) / k ]_ A = C )
17 16 eqcomd 
 |-  ( ( ph /\ i e. ( M ... N ) ) -> C = [_ ( i + 1 ) / k ]_ A )
18 13 17 oveq12d 
 |-  ( ( ph /\ i e. ( M ... N ) ) -> ( L .- C ) = ( [_ i / k ]_ A .- [_ ( i + 1 ) / k ]_ A ) )
19 18 mpteq2dva 
 |-  ( ph -> ( i e. ( M ... N ) |-> ( L .- C ) ) = ( i e. ( M ... N ) |-> ( [_ i / k ]_ A .- [_ ( i + 1 ) / k ]_ A ) ) )
20 19 oveq2d 
 |-  ( ph -> ( G gsum ( i e. ( M ... N ) |-> ( L .- C ) ) ) = ( G gsum ( i e. ( M ... N ) |-> ( [_ i / k ]_ A .- [_ ( i + 1 ) / k ]_ A ) ) ) )
21 1 2 3 4 5 telgsumfzs 
 |-  ( ph -> ( G gsum ( i e. ( M ... N ) |-> ( [_ i / k ]_ A .- [_ ( i + 1 ) / k ]_ A ) ) ) = ( [_ M / k ]_ A .- [_ ( N + 1 ) / k ]_ A ) )
22 4 elfvexd 
 |-  ( ph -> M e. _V )
23 8 adantl 
 |-  ( ( ph /\ k = M ) -> A = D )
24 22 23 csbied 
 |-  ( ph -> [_ M / k ]_ A = D )
25 ovexd 
 |-  ( ph -> ( N + 1 ) e. _V )
26 9 adantl 
 |-  ( ( ph /\ k = ( N + 1 ) ) -> A = E )
27 25 26 csbied 
 |-  ( ph -> [_ ( N + 1 ) / k ]_ A = E )
28 24 27 oveq12d 
 |-  ( ph -> ( [_ M / k ]_ A .- [_ ( N + 1 ) / k ]_ A ) = ( D .- E ) )
29 20 21 28 3eqtrd 
 |-  ( ph -> ( G gsum ( i e. ( M ... N ) |-> ( L .- C ) ) ) = ( D .- E ) )