Metamath Proof Explorer

Theorem itgeq2

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

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  RR = RR
2 simpl 
 |-  ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) -> x e. A )
3 2 con3i 
 |-  ( -. x e. A -> -. ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) )
4 3 iffalsed 
 |-  ( -. x e. A -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) = 0 )
5 simpl 
 |-  ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) -> x e. A )
6 5 con3i 
 |-  ( -. x e. A -> -. ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) )
7 6 iffalsed 
 |-  ( -. x e. A -> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = 0 )
8 4 7 eqtr4d 
 |-  ( -. x e. A -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
9 fvoveq1 
 |-  ( B = C -> ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) ) )
10 9 breq2d 
 |-  ( B = C -> ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) <-> 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) )
11 10 anbi2d 
 |-  ( B = C -> ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) <-> ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) ) )
12 11 9 ifbieq1d 
 |-  ( B = C -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
13 8 12 ja 
 |-  ( ( x e. A -> B = C ) -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
14 13 a1d 
 |-  ( ( x e. A -> B = C ) -> ( x e. RR -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
15 14 ralimi2 
 |-  ( A. x e. A B = C -> A. x e. RR if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
16 mpteq12 
 |-  ( ( RR = RR /\ A. x e. RR if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
17 1 15 16 sylancr 
 |-  ( A. x e. A B = C -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
18 17 fveq2d 
 |-  ( A. x e. A B = C -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
19 18 oveq2d 
 |-  ( A. x e. A B = C -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) )
20 19 sumeq2sdv 
 |-  ( A. x e. A B = C -> sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) )
21 eqid 
 |-  ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) )
22 21 dfitg 
 |-  S. A B _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) )
23 eqid 
 |-  ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) )
24 23 dfitg 
 |-  S. A C _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
25 20 22 24 3eqtr4g 
 |-  ( A. x e. A B = C -> S. A B _d x = S. A C _d x )