Metamath Proof Explorer

Theorem itgresr

Description: The domain of an integral only matters in its intersection with RR . (Contributed by Mario Carneiro, 29-Jun-2014)

Ref Expression
Assertion itgresr 
|- S. A B _d x = S. ( A i^i RR ) B _d x

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( k e. ( 0 ... 3 ) /\ x e. RR ) -> x e. RR )
2 1 biantrud 
 |-  ( ( k e. ( 0 ... 3 ) /\ x e. RR ) -> ( x e. A <-> ( x e. A /\ x e. RR ) ) )
3 elin 
 |-  ( x e. ( A i^i RR ) <-> ( x e. A /\ x e. RR ) )
4 2 3 bitr4di 
 |-  ( ( k e. ( 0 ... 3 ) /\ x e. RR ) -> ( x e. A <-> x e. ( A i^i RR ) ) )
5 4 anbi1d 
 |-  ( ( k e. ( 0 ... 3 ) /\ x e. RR ) -> ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) <-> ( x e. ( A i^i RR ) /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) ) )
6 5 ifbid 
 |-  ( ( k e. ( 0 ... 3 ) /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. ( A i^i RR ) /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) )
7 6 mpteq2dva 
 |-  ( k e. ( 0 ... 3 ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. ( A i^i RR ) /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) )
8 7 fveq2d 
 |-  ( k e. ( 0 ... 3 ) -> ( 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 i^i RR ) /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) )
9 8 oveq2d 
 |-  ( 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 ) ) ) ) = ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. ( A i^i RR ) /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) )
10 9 sumeq2i 
 |-  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 i^i RR ) /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) )
11 eqid 
 |-  ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) )
12 11 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 ) ) ) )
13 11 dfitg 
 |-  S. ( A i^i RR ) B _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. ( A i^i RR ) /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) )
14 10 12 13 3eqtr4i 
 |-  S. A B _d x = S. ( A i^i RR ) B _d x