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 )