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

Metamath Proof Explorer

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 )