Metamath Proof Explorer


Theorem cbvsum

Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jun-2019)

Ref Expression
Hypotheses cbvsum.1 j=kB=C
cbvsum.2 _kA
cbvsum.3 _jA
cbvsum.4 _kB
cbvsum.5 _jC
Assertion cbvsum jAB=kAC

Proof

Step Hyp Ref Expression
1 cbvsum.1 j=kB=C
2 cbvsum.2 _kA
3 cbvsum.3 _jA
4 cbvsum.4 _kB
5 cbvsum.5 _jC
6 4 5 1 cbvcsbw n/jB=n/kC
7 6 a1i n/jB=n/kC
8 7 ifeq1d ifnAn/jB0=ifnAn/kC0
9 8 mpteq2dv nifnAn/jB0=nifnAn/kC0
10 9 seqeq3d seqm+nifnAn/jB0=seqm+nifnAn/kC0
11 10 mptru seqm+nifnAn/jB0=seqm+nifnAn/kC0
12 11 breq1i seqm+nifnAn/jB0xseqm+nifnAn/kC0x
13 12 anbi2i Amseqm+nifnAn/jB0xAmseqm+nifnAn/kC0x
14 13 rexbii mAmseqm+nifnAn/jB0xmAmseqm+nifnAn/kC0x
15 4 5 1 cbvcsbw fn/jB=fn/kC
16 15 a1i fn/jB=fn/kC
17 16 mpteq2dv nfn/jB=nfn/kC
18 17 seqeq3d seq1+nfn/jB=seq1+nfn/kC
19 18 mptru seq1+nfn/jB=seq1+nfn/kC
20 19 fveq1i seq1+nfn/jBm=seq1+nfn/kCm
21 20 eqeq2i x=seq1+nfn/jBmx=seq1+nfn/kCm
22 21 anbi2i f:1m1-1 ontoAx=seq1+nfn/jBmf:1m1-1 ontoAx=seq1+nfn/kCm
23 22 exbii ff:1m1-1 ontoAx=seq1+nfn/jBmff:1m1-1 ontoAx=seq1+nfn/kCm
24 23 rexbii mff:1m1-1 ontoAx=seq1+nfn/jBmmff:1m1-1 ontoAx=seq1+nfn/kCm
25 14 24 orbi12i mAmseqm+nifnAn/jB0xmff:1m1-1 ontoAx=seq1+nfn/jBmmAmseqm+nifnAn/kC0xmff:1m1-1 ontoAx=seq1+nfn/kCm
26 25 iotabii ιx|mAmseqm+nifnAn/jB0xmff:1m1-1 ontoAx=seq1+nfn/jBm=ιx|mAmseqm+nifnAn/kC0xmff:1m1-1 ontoAx=seq1+nfn/kCm
27 df-sum jAB=ιx|mAmseqm+nifnAn/jB0xmff:1m1-1 ontoAx=seq1+nfn/jBm
28 df-sum kAC=ιx|mAmseqm+nifnAn/kC0xmff:1m1-1 ontoAx=seq1+nfn/kCm
29 26 27 28 3eqtr4i jAB=kAC