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 B
cbvsum.3 
|- 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 B
3 cbvsum.3 
 |-  F/_ j C
4 2 3 1 cbvcsbw 
 |-  [_ n / j ]_ B = [_ n / k ]_ C
5 4 a1i 
 |-  ( T. -> [_ n / j ]_ B = [_ n / k ]_ C )
6 5 ifeq1d 
 |-  ( T. -> if ( n e. A , [_ n / j ]_ B , 0 ) = if ( n e. A , [_ n / k ]_ C , 0 ) )
7 6 mpteq2dv 
 |-  ( T. -> ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ B , 0 ) ) = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) )
8 7 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 ) ) ) )
9 8 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 ) ) )
10 9 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 )
11 10 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 ) )
12 11 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 ) )
13 2 3 1 cbvcsbw 
 |-  [_ ( f ` n ) / j ]_ B = [_ ( f ` n ) / k ]_ C
14 13 a1i 
 |-  ( T. -> [_ ( f ` n ) / j ]_ B = [_ ( f ` n ) / k ]_ C )
15 14 mpteq2dv 
 |-  ( T. -> ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) = ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) )
16 15 seqeq3d 
 |-  ( T. -> seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) = seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) )
17 16 mptru 
 |-  seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) = seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) )
18 17 fveq1i 
 |-  ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m )
19 18 eqeq2i 
 |-  ( x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) <-> x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) )
20 19 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 ) ) )
21 20 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 ) ) )
22 21 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 ) ) )
23 12 22 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 ) ) ) )
24 23 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 ) ) ) )
25 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 ) ) ) )
26 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 ) ) ) )
27 24 25 26 3eqtr4i 
 |-  sum_ j e. A B = sum_ k e. A C