# 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 = k -> B = C )`
cbvsum.2
`|- F/_ k A`
cbvsum.3
`|- F/_ j A`
cbvsum.4
`|- F/_ k B`
cbvsum.5
`|- F/_ j C`
Assertion cbvsum
`|- sum_ j e. A B = sum_ k e. A C`

### Proof

Step Hyp Ref Expression
1 cbvsum.1
` |-  ( j = k -> B = C )`
2 cbvsum.2
` |-  F/_ k A`
3 cbvsum.3
` |-  F/_ j A`
4 cbvsum.4
` |-  F/_ k B`
5 cbvsum.5
` |-  F/_ j C`
6 4 5 1 cbvcsbw
` |-  [_ n / j ]_ B = [_ n / k ]_ C`
7 6 a1i
` |-  ( T. -> [_ n / j ]_ B = [_ n / k ]_ C )`
8 7 ifeq1d
` |-  ( T. -> if ( n e. A , [_ n / j ]_ B , 0 ) = if ( n e. A , [_ n / k ]_ C , 0 ) )`
9 8 mpteq2dv
` |-  ( T. -> ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) )`
10 9 seqeq3d
` |-  ( T. -> seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) ) = seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) )`
11 10 mptru
` |-  seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) ) = seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) )`
12 11 breq1i
` |-  ( seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) ) ~~> x <-> seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x )`
13 12 anbi2i
` |-  ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) ) ~~> x ) <-> ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) )`
14 13 rexbii
` |-  ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) ) ~~> x ) <-> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) )`
15 4 5 1 cbvcsbw
` |-  [_ ( f ` n ) / j ]_ B = [_ ( f ` n ) / k ]_ C`
16 15 a1i
` |-  ( T. -> [_ ( f ` n ) / j ]_ B = [_ ( f ` n ) / k ]_ C )`
17 16 mpteq2dv
` |-  ( T. -> ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) = ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) )`
18 17 seqeq3d
` |-  ( T. -> seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) = seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) )`
19 18 mptru
` |-  seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) = seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) )`
20 19 fveq1i
` |-  ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m )`
21 20 eqeq2i
` |-  ( x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) <-> x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) )`
22 21 anbi2i
` |-  ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) )`
23 22 exbii
` |-  ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) )`
24 23 rexbii
` |-  ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) ) <-> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) )`
25 14 24 orbi12i
` |-  ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) ) ) <-> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )`
26 25 iotabii
` |-  ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) ) ) ) = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )`
27 df-sum
` |-  sum_ j e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) ) ) )`
28 df-sum
` |-  sum_ k e. A C = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )`
29 26 27 28 3eqtr4i
` |-  sum_ j e. A B = sum_ k e. A C`