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

Metamath Proof Explorer

Theorem telgsumfz0

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

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

Proof

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