Metamath Proof Explorer

Theorem sumeq2sdv

Description: Equality deduction for sum. (Contributed by NM, 3-Jan-2006) (Proof shortened by Glauco Siliprandi, 5-Apr-2020) Avoid axioms. (Revised by GG, 14-Aug-2025)

Ref Expression
Hypothesis sumeq2sdv.1 
|- ( ph -> B = C )
Assertion sumeq2sdv 
|- ( ph -> sum_ k e. A B = sum_ k e. A C )

Proof

Step Hyp Ref Expression
1 sumeq2sdv.1 
 |-  ( ph -> B = C )
2 1 csbeq2dv 
 |-  ( ph -> [_ n / k ]_ B = [_ n / k ]_ C )
3 2 ifeq1d 
 |-  ( ph -> if ( n e. A , [_ n / k ]_ B , 0 ) = if ( n e. A , [_ n / k ]_ C , 0 ) )
4 3 mpteq2dv 
 |-  ( ph -> ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) )
5 4 seqeq3d 
 |-  ( ph -> seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) = seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) )
6 5 breq1d 
 |-  ( ph -> ( seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x <-> seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) )
7 6 anbi2d 
 |-  ( ph -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) <-> ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) ) )
8 7 rexbidv 
 |-  ( ph -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ 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 ) ) )
9 1 csbeq2dv 
 |-  ( ph -> [_ ( f ` n ) / k ]_ B = [_ ( f ` n ) / k ]_ C )
10 9 mpteq2dv 
 |-  ( ph -> ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) )
11 10 seqeq3d 
 |-  ( ph -> seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) = seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) )
12 11 fveq1d 
 |-  ( ph -> ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) )
13 12 eqeq2d 
 |-  ( ph -> ( x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) <-> x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) )
14 13 anbi2d 
 |-  ( ph -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )
15 14 exbidv 
 |-  ( ph -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )
16 15 rexbidv 
 |-  ( ph -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ 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 ) ) ) )
17 8 16 orbi12d 
 |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ 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 ) ) ) ) )
18 17 iotabidv 
 |-  ( ph -> ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ 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 ) ) ) ) )
19 df-sum 
 |-  sum_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
20 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 ) ) ) )
21 18 19 20 3eqtr4g 
 |-  ( ph -> sum_ k e. A B = sum_ k e. A C )