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