Theorem fprodshft

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

	Ref	Expression
Hypotheses	fprodshft.1	$$⊢\phi \to K\in \mathbb{Z}$$
	fprodshft.2	$$⊢\phi \to M\in \mathbb{Z}$$
	fprodshft.3	$$⊢\phi \to N\in \mathbb{Z}$$
	fprodshft.4	$$⊢\left(\phi \wedge j\in \left(M\dots N\right)\right)\to A\in ℂ$$
	fprodshft.5	$$⊢j=k-K\to A=B$$
Assertion	fprodshft	$$⊢\phi \to \prod _{j=M}^{N}A=\prod _{k=M+K}^{N+K}B$$

Proof

Step	Hyp	Ref	Expression
1		fprodshft.1	$$⊢\phi \to K\in \mathbb{Z}$$
2		fprodshft.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		fprodshft.3	$$⊢\phi \to N\in \mathbb{Z}$$
4		fprodshft.4	$$⊢\left(\phi \wedge j\in \left(M\dots N\right)\right)\to A\in ℂ$$
5		fprodshft.5	$$⊢j=k-K\to A=B$$
6		fzfid	$$⊢\phi \to \left(M+K\dots N+K\right)\in \mathrm{Fin}$$
7	1 2 3	mptfzshft	$$⊢\phi \to \left(j\in \left(M+K\dots N+K\right)⟼j-K\right):\left(M+K\dots N+K\right)\underset{1-1\; onto}{⟶}\left(M\dots N\right)$$
8		oveq1	$$⊢j=k\to j-K=k-K$$
9		eqid	$$⊢\left(j\in \left(M+K\dots N+K\right)⟼j-K\right)=\left(j\in \left(M+K\dots N+K\right)⟼j-K\right)$$
10		ovex	$$⊢k-K\in \mathrm{V}$$
11	8 9 10	fvmpt	$$⊢k\in \left(M+K\dots N+K\right)\to \left(j\in \left(M+K\dots N+K\right)⟼j-K\right)\left(k\right)=k-K$$
12	11	adantl	$$⊢\left(\phi \wedge k\in \left(M+K\dots N+K\right)\right)\to \left(j\in \left(M+K\dots N+K\right)⟼j-K\right)\left(k\right)=k-K$$
13	5 6 7 12 4	fprodf1o	$$⊢\phi \to \prod _{j=M}^{N}A=\prod _{k=M+K}^{N+K}B$$