Metamath Proof Explorer

Theorem sumeq1

Description: Equality theorem for a sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jun-2019)

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

Proof

Step	Hyp	Ref	Expression
1		sseq1	\|- ( A = B -> ( A C_ ( ZZ>= ` m ) <-> B C_ ( ZZ>= ` m ) ) )
2		simpl	\|- ( ( A = B /\ n e. ZZ ) -> A = B )
3	2	eleq2d	\|- ( ( A = B /\ n e. ZZ ) -> ( n e. A <-> n e. B ) )
4	3	ifbid	\|- ( ( A = B /\ n e. ZZ ) -> if ( n e. A , [_ n / k ]_ C , 0 ) = if ( n e. B , [_ n / k ]_ C , 0 ) )
5	4	mpteq2dva	\|- ( A = B -> ( n e. ZZ \|-> if ( n e. A , [_ n / k ]_ C , 0 ) ) = ( n e. ZZ \|-> if ( n e. B , [_ n / k ]_ C , 0 ) ) )
6	5	seqeq3d	\|- ( A = B -> seq m ( + , ( n e. ZZ \|-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) = seq m ( + , ( n e. ZZ \|-> if ( n e. B , [_ n / k ]_ C , 0 ) ) ) )
7	6	breq1d	\|- ( A = B -> ( seq m ( + , ( n e. ZZ \|-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x <-> seq m ( + , ( n e. ZZ \|-> if ( n e. B , [_ n / k ]_ C , 0 ) ) ) ~~> x ) )
8	1 7	anbi12d	\|- ( A = B -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ \|-> if ( n e. A , [_ n / k ]_ C , 0 ) ) ) ~~> x ) <-> ( B C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ \|-> if ( n e. B , [_ n / k ]_ C , 0 ) ) ) ~~> x ) ) )
9	8	rexbidv	\|- ( A = B -> ( 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. ZZ ( B C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ \|-> if ( n e. B , [_ n / k ]_ C , 0 ) ) ) ~~> x ) ) )
10		f1oeq3	\|- ( A = B -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... m ) -1-1-onto-> B ) )
11	10	anbi1d	\|- ( A = B -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN \|-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( + , ( n e. NN \|-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )
12	11	exbidv	\|- ( A = B -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN \|-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( + , ( n e. NN \|-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )
13	12	rexbidv	\|- ( A = B -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN \|-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) <-> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( + , ( n e. NN \|-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )
14	9 13	orbi12d	\|- ( A = B -> ( ( 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 ) ) ) <-> ( E. m e. ZZ ( B C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ \|-> if ( n e. B , [_ n / k ]_ C , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( + , ( n e. NN \|-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) ) )
15	14	iotabidv	\|- ( A = B -> ( 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 ) ) ) ) = ( iota x ( E. m e. ZZ ( B C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ \|-> if ( n e. B , [_ n / k ]_ C , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( + , ( n e. NN \|-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) ) )
16		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 ) ) ) )
17		df-sum	\|- sum_ k e. B C = ( iota x ( E. m e. ZZ ( B C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ \|-> if ( n e. B , [_ n / k ]_ C , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( + , ( n e. NN \|-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )
18	15 16 17	3eqtr4g	\|- ( A = B -> sum_ k e. A C = sum_ k e. B C )