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