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