This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sumeq2w

Description: Equality theorem for sum, when the class expressions B and C are equal everywhere. Proved using only Extensionality. (Contributed by Mario Carneiro, 24-Jun-2014) (Revised by Mario Carneiro, 13-Jun-2019)

Ref Expression
Assertion sumeq2w 
|- ( A. k B = C -> sum_ k e. A B = sum_ k e. A C )

Proof

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