Metamath Proof Explorer

Theorem telgsum

Description: Telescoping finitely supported group sum ranging over nonnegative integers, using implicit substitution. (Contributed by AV, 31-Dec-2019)

Ref Expression
Hypotheses telgsum.b 
|- B = ( Base ` G )
telgsum.g 
|- ( ph -> G e. Abel )
telgsum.m 
|- .- = ( -g ` G )
telgsum.0 
|- .0. = ( 0g ` G )
telgsum.f 
|- ( ph -> A. k e. NN0 A e. B )
telgsum.s 
|- ( ph -> S e. NN0 )
telgsum.u 
|- ( ph -> A. k e. NN0 ( S < k -> A = .0. ) )
telgsum.c 
|- ( k = i -> A = C )
telgsum.d 
|- ( k = ( i + 1 ) -> A = D )
telgsum.e 
|- ( k = 0 -> A = E )
Assertion telgsum 
|- ( ph -> ( G gsum ( i e. NN0 |-> ( C .- D ) ) ) = E )

Proof

Step Hyp Ref Expression
1 telgsum.b 
 |-  B = ( Base ` G )
2 telgsum.g 
 |-  ( ph -> G e. Abel )
3 telgsum.m 
 |-  .- = ( -g ` G )
4 telgsum.0 
 |-  .0. = ( 0g ` G )
5 telgsum.f 
 |-  ( ph -> A. k e. NN0 A e. B )
6 telgsum.s 
 |-  ( ph -> S e. NN0 )
7 telgsum.u 
 |-  ( ph -> A. k e. NN0 ( S < k -> A = .0. ) )
8 telgsum.c 
 |-  ( k = i -> A = C )
9 telgsum.d 
 |-  ( k = ( i + 1 ) -> A = D )
10 telgsum.e 
 |-  ( k = 0 -> A = E )
11 simpr 
 |-  ( ( ph /\ i e. NN0 ) -> i e. NN0 )
12 8 adantl 
 |-  ( ( ( ph /\ i e. NN0 ) /\ k = i ) -> A = C )
13 11 12 csbied 
 |-  ( ( ph /\ i e. NN0 ) -> [_ i / k ]_ A = C )
14 13 eqcomd 
 |-  ( ( ph /\ i e. NN0 ) -> C = [_ i / k ]_ A )
15 peano2nn0 
 |-  ( i e. NN0 -> ( i + 1 ) e. NN0 )
16 15 adantl 
 |-  ( ( ph /\ i e. NN0 ) -> ( i + 1 ) e. NN0 )
17 9 adantl 
 |-  ( ( ( ph /\ i e. NN0 ) /\ k = ( i + 1 ) ) -> A = D )
18 16 17 csbied 
 |-  ( ( ph /\ i e. NN0 ) -> [_ ( i + 1 ) / k ]_ A = D )
19 18 eqcomd 
 |-  ( ( ph /\ i e. NN0 ) -> D = [_ ( i + 1 ) / k ]_ A )
20 14 19 oveq12d 
 |-  ( ( ph /\ i e. NN0 ) -> ( C .- D ) = ( [_ i / k ]_ A .- [_ ( i + 1 ) / k ]_ A ) )
21 20 mpteq2dva 
 |-  ( ph -> ( i e. NN0 |-> ( C .- D ) ) = ( i e. NN0 |-> ( [_ i / k ]_ A .- [_ ( i + 1 ) / k ]_ A ) ) )
22 21 oveq2d 
 |-  ( ph -> ( G gsum ( i e. NN0 |-> ( C .- D ) ) ) = ( G gsum ( i e. NN0 |-> ( [_ i / k ]_ A .- [_ ( i + 1 ) / k ]_ A ) ) ) )
23 1 2 3 4 5 6 7 telgsums 
 |-  ( ph -> ( G gsum ( i e. NN0 |-> ( [_ i / k ]_ A .- [_ ( i + 1 ) / k ]_ A ) ) ) = [_ 0 / k ]_ A )
24 c0ex 
 |-  0 e. _V
25 24 a1i 
 |-  ( ph -> 0 e. _V )
26 10 adantl 
 |-  ( ( ph /\ k = 0 ) -> A = E )
27 25 26 csbied 
 |-  ( ph -> [_ 0 / k ]_ A = E )
28 22 23 27 3eqtrd 
 |-  ( ph -> ( G gsum ( i e. NN0 |-> ( C .- D ) ) ) = E )