Metamath Proof Explorer

Theorem fsumshftd

Description: Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft . The proof demonstrates how this can be derived starting from from fsumshft . (Contributed by NM, 1-Nov-2019)

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

Proof

Step Hyp Ref Expression
1 fsumshftd.1 
 |-  ( ph -> K e. ZZ )
2 fsumshftd.2 
 |-  ( ph -> M e. ZZ )
3 fsumshftd.3 
 |-  ( ph -> N e. ZZ )
4 fsumshftd.4 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )
5 fsumshftd.5 
 |-  ( ( ph /\ j = ( k - K ) ) -> A = B )
6 nfcv 
 |-  F/_ w A
7 nfcsb1v 
 |-  F/_ j [_ w / j ]_ A
8 csbeq1a 
 |-  ( j = w -> A = [_ w / j ]_ A )
9 6 7 8 cbvsumi 
 |-  sum_ j e. ( M ... N ) A = sum_ w e. ( M ... N ) [_ w / j ]_ A
10 nfv 
 |-  F/ j ( ph /\ w e. ( M ... N ) )
11 7 nfel1 
 |-  F/ j [_ w / j ]_ A e. CC
12 10 11 nfim 
 |-  F/ j ( ( ph /\ w e. ( M ... N ) ) -> [_ w / j ]_ A e. CC )
13 eleq1w 
 |-  ( j = w -> ( j e. ( M ... N ) <-> w e. ( M ... N ) ) )
14 13 anbi2d 
 |-  ( j = w -> ( ( ph /\ j e. ( M ... N ) ) <-> ( ph /\ w e. ( M ... N ) ) ) )
15 8 eleq1d 
 |-  ( j = w -> ( A e. CC <-> [_ w / j ]_ A e. CC ) )
16 14 15 imbi12d 
 |-  ( j = w -> ( ( ( ph /\ j e. ( M ... N ) ) -> A e. CC ) <-> ( ( ph /\ w e. ( M ... N ) ) -> [_ w / j ]_ A e. CC ) ) )
17 12 16 4 chvarfv 
 |-  ( ( ph /\ w e. ( M ... N ) ) -> [_ w / j ]_ A e. CC )
18 csbeq1 
 |-  ( w = ( k - K ) -> [_ w / j ]_ A = [_ ( k - K ) / j ]_ A )
19 1 2 3 17 18 fsumshft 
 |-  ( ph -> sum_ w e. ( M ... N ) [_ w / j ]_ A = sum_ k e. ( ( M + K ) ... ( N + K ) ) [_ ( k - K ) / j ]_ A )
20 ovexd 
 |-  ( ph -> ( k - K ) e. _V )
21 20 5 csbied 
 |-  ( ph -> [_ ( k - K ) / j ]_ A = B )
22 21 sumeq2sdv 
 |-  ( ph -> sum_ k e. ( ( M + K ) ... ( N + K ) ) [_ ( k - K ) / j ]_ A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B )
23 19 22 eqtrd 
 |-  ( ph -> sum_ w e. ( M ... N ) [_ w / j ]_ A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B )
24 9 23 syl5eq 
 |-  ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B )