Theorem fprodshft

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

	Ref	Expression
Hypotheses	fprodshft.1	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
	fprodshft.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	fprodshft.3	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	fprodshft.4	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
	fprodshft.5	⊢ ( 𝑗 = ( 𝑘 − 𝐾 ) → 𝐴 = 𝐵 )
Assertion	fprodshft	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ∏ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fprodshft.1	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
2		fprodshft.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		fprodshft.3	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4		fprodshft.4	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
5		fprodshft.5	⊢ ( 𝑗 = ( 𝑘 − 𝐾 ) → 𝐴 = 𝐵 )
6		fzfid	⊢ ( 𝜑 → ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∈ Fin )
7	1 2 3	mptfzshft	⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) : ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )
8		oveq1	⊢ ( 𝑗 = 𝑘 → ( 𝑗 − 𝐾 ) = ( 𝑘 − 𝐾 ) )
9		eqid	⊢ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) = ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) )
10		ovex	⊢ ( 𝑘 − 𝐾 ) ∈ V
11	8 9 10	fvmpt	⊢ ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) → ( ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) ‘ 𝑘 ) = ( 𝑘 − 𝐾 ) )
12	11	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → ( ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) ‘ 𝑘 ) = ( 𝑘 − 𝐾 ) )
13	5 6 7 12 4	fprodf1o	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ∏ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) 𝐵 )