Metamath Proof Explorer


Theorem fsumshft

Description: Index shift of a finite sum. (Contributed by NM, 27-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014) (Proof shortened by AV, 8-Sep-2019)

Ref Expression
Hypotheses fsumrev.1
|- ( ph -> K e. ZZ )
fsumrev.2
|- ( ph -> M e. ZZ )
fsumrev.3
|- ( ph -> N e. ZZ )
fsumrev.4
|- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )
fsumshft.5
|- ( j = ( k - K ) -> A = B )
Assertion fsumshft
|- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B )

Proof

Step Hyp Ref Expression
1 fsumrev.1
 |-  ( ph -> K e. ZZ )
2 fsumrev.2
 |-  ( ph -> M e. ZZ )
3 fsumrev.3
 |-  ( ph -> N e. ZZ )
4 fsumrev.4
 |-  ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )
5 fsumshft.5
 |-  ( j = ( k - K ) -> A = B )
6 fzfid
 |-  ( ph -> ( ( M + K ) ... ( N + K ) ) e. Fin )
7 1 2 3 mptfzshft
 |-  ( ph -> ( j e. ( ( M + K ) ... ( N + K ) ) |-> ( j - K ) ) : ( ( M + K ) ... ( N + K ) ) -1-1-onto-> ( M ... N ) )
8 oveq1
 |-  ( j = k -> ( j - K ) = ( k - K ) )
9 eqid
 |-  ( j e. ( ( M + K ) ... ( N + K ) ) |-> ( j - K ) ) = ( j e. ( ( M + K ) ... ( N + K ) ) |-> ( j - K ) )
10 ovex
 |-  ( k - K ) e. _V
11 8 9 10 fvmpt
 |-  ( k e. ( ( M + K ) ... ( N + K ) ) -> ( ( j e. ( ( M + K ) ... ( N + K ) ) |-> ( j - K ) ) ` k ) = ( k - K ) )
12 11 adantl
 |-  ( ( ph /\ k e. ( ( M + K ) ... ( N + K ) ) ) -> ( ( j e. ( ( M + K ) ... ( N + K ) ) |-> ( j - K ) ) ` k ) = ( k - K ) )
13 5 6 7 12 4 fsumf1o
 |-  ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B )