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 φ K
fsumshftd.2 φ M
fsumshftd.3 φ N
fsumshftd.4 φ j M N A
fsumshftd.5 φ j = k K A = B
Assertion fsumshftd φ j = M N A = k = M + K N + K B

Proof

Step Hyp Ref Expression
1 fsumshftd.1 φ K
2 fsumshftd.2 φ M
3 fsumshftd.3 φ N
4 fsumshftd.4 φ j M N A
5 fsumshftd.5 φ j = k K A = B
6 nfcv _ w A
7 nfcsb1v _ j w / j A
8 csbeq1a j = w A = w / j A
9 6 7 8 cbvsumi j = M N A = w = M N w / j A
10 nfv j φ w M N
11 7 nfel1 j w / j A
12 10 11 nfim j φ w M N w / j A
13 eleq1w j = w j M N w M N
14 13 anbi2d j = w φ j M N φ w M N
15 8 eleq1d j = w A w / j A
16 14 15 imbi12d j = w φ j M N A φ w M N w / j A
17 12 16 4 chvarfv φ w M N w / j A
18 csbeq1 w = k K w / j A = k K / j A
19 1 2 3 17 18 fsumshft φ w = M N w / j A = k = M + K N + K k K / j A
20 ovexd φ k K V
21 20 5 csbied φ k K / j A = B
22 21 sumeq2sdv φ k = M + K N + K k K / j A = k = M + K N + K B
23 19 22 eqtrd φ w = M N w / j A = k = M + K N + K B
24 9 23 eqtrid φ j = M N A = k = M + K N + K B