This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )