Metamath Proof Explorer

Theorem cbvsumdavw2

Description: Change bound variable and the set of integers in a sum. Deduction form. (Contributed by GG, 14-Aug-2025)

Ref Expression
Hypotheses cbvsumdavw2.1 
|- ( ph -> A = B )
cbvsumdavw2.2 
|- ( ( ph /\ j = k ) -> C = D )
Assertion cbvsumdavw2 
|- ( ph -> sum_ j e. A C = sum_ k e. B D )

Proof

Step Hyp Ref Expression
1 cbvsumdavw2.1 
 |-  ( ph -> A = B )
2 cbvsumdavw2.2 
 |-  ( ( ph /\ j = k ) -> C = D )
3 1 sseq1d 
 |-  ( ph -> ( A C_ ( ZZ>= ` m ) <-> B C_ ( ZZ>= ` m ) ) )
4 1 eleq2d 
 |-  ( ph -> ( n e. A <-> n e. B ) )
5 2 cbvcsbdavw 
 |-  ( ph -> [_ n / j ]_ C = [_ n / k ]_ D )
6 4 5 ifbieq1d 
 |-  ( ph -> if ( n e. A , [_ n / j ]_ C , 0 ) = if ( n e. B , [_ n / k ]_ D , 0 ) )
7 6 mpteq2dv 
 |-  ( ph -> ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ C , 0 ) ) = ( n e. ZZ |-> if ( n e. B , [_ n / k ]_ D , 0 ) ) )
8 7 seqeq3d 
 |-  ( ph -> seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ C , 0 ) ) ) = seq m ( + , ( n e. ZZ |-> if ( n e. B , [_ n / k ]_ D , 0 ) ) ) )
9 8 breq1d 
 |-  ( ph -> ( seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ C , 0 ) ) ) ~~> x <-> seq m ( + , ( n e. ZZ |-> if ( n e. B , [_ n / k ]_ D , 0 ) ) ) ~~> x ) )
10 3 9 anbi12d 
 |-  ( ph -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ C , 0 ) ) ) ~~> x ) <-> ( B C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. B , [_ n / k ]_ D , 0 ) ) ) ~~> x ) ) )
11 10 rexbidv 
 |-  ( ph -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ C , 0 ) ) ) ~~> x ) <-> E. m e. ZZ ( B C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. B , [_ n / k ]_ D , 0 ) ) ) ~~> x ) ) )
12 1 f1oeq3d 
 |-  ( ph -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... m ) -1-1-onto-> B ) )
13 2 cbvcsbdavw 
 |-  ( ph -> [_ ( f ` n ) / j ]_ C = [_ ( f ` n ) / k ]_ D )
14 13 mpteq2dv 
 |-  ( ph -> ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) = ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) )
15 14 seqeq3d 
 |-  ( ph -> seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) = seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) )
16 15 fveq1d 
 |-  ( ph -> ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) )
17 16 eqeq2d 
 |-  ( ph -> ( x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) <-> x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) ) )
18 12 17 anbi12d 
 |-  ( ph -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) ) ) )
19 18 exbidv 
 |-  ( ph -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) ) ) )
20 19 rexbidv 
 |-  ( ph -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) ) <-> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) ) ) )
21 11 20 orbi12d 
 |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ C , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) ) ) <-> ( E. m e. ZZ ( B C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. B , [_ n / k ]_ D , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) ) ) ) )
22 21 iotabidv 
 |-  ( ph -> ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ C , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) ) ) ) = ( iota x ( E. m e. ZZ ( B C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. B , [_ n / k ]_ D , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) ) ) ) )
23 df-sum 
 |-  sum_ j e. A C = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / j ]_ C , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) ) ) )
24 df-sum 
 |-  sum_ k e. B D = ( iota x ( E. m e. ZZ ( B C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. B , [_ n / k ]_ D , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) ) ) )
25 22 23 24 3eqtr4g 
 |-  ( ph -> sum_ j e. A C = sum_ k e. B D )