Theorem fprodshft

Description: Shift the index of a finite product. (Contributed by Scott Fenton, 5-Jan-2018)

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

Proof

Step	Hyp	Ref	Expression
1		fprodshft.1	|- ( ph -> K e. ZZ )
2		fprodshft.2	|- ( ph -> M e. ZZ )
3		fprodshft.3	|- ( ph -> N e. ZZ )
4		fprodshft.4	|- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )
5		fprodshft.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	fprodf1o	|- ( ph -> prod_ j e. ( M ... N ) A = prod_ k e. ( ( M + K ) ... ( N + K ) ) B )