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 )