Theorem itgeq1

Description: Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Assertion	itgeq1	|- ( A = B -> S. A C _d x = S. B C _d x )

Proof

Step	Hyp	Ref	Expression
1		eleq2	|- ( A = B -> ( x e. A <-> x e. B ) )
2	1	anbi1d	|- ( A = B -> ( ( x e. A /\ 0 <_ y ) <-> ( x e. B /\ 0 <_ y ) ) )
3	2	ifbid	|- ( A = B -> if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = if ( ( x e. B /\ 0 <_ y ) , y , 0 ) )
4	3	csbeq2dv	|- ( A = B -> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) )
5	4	mpteq2dv	|- ( A = B -> ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) = ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) )
6	5	fveq2d	|- ( A = B -> ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) = ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) ) )
7	6	oveq2d	|- ( A = B -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) ) = ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) ) ) )
8	7	sumeq2sdv	|- ( A = B -> sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) ) = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) ) ) )
9		df-itg	|- S. A C _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) )
10		df-itg	|- S. B C _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) ) )
11	8 9 10	3eqtr4g	|- ( A = B -> S. A C _d x = S. B C _d x )