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

Metamath Proof Explorer

Theorem dfitg

Description: Evaluate the class substitution in df-itg . (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypothesis dfitg.1 
|- T = ( Re ` ( B / ( _i ^ k ) ) )
Assertion dfitg 
|- S. A B _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 dfitg.1 
 |-  T = ( Re ` ( B / ( _i ^ k ) ) )
2 df-itg 
 |-  S. A B _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) )
3 fvex 
 |-  ( Re ` ( B / ( _i ^ k ) ) ) e. _V
4 id 
 |-  ( y = ( Re ` ( B / ( _i ^ k ) ) ) -> y = ( Re ` ( B / ( _i ^ k ) ) ) )
5 4 1 eqtr4di 
 |-  ( y = ( Re ` ( B / ( _i ^ k ) ) ) -> y = T )
6 5 breq2d 
 |-  ( y = ( Re ` ( B / ( _i ^ k ) ) ) -> ( 0 <_ y <-> 0 <_ T ) )
7 6 anbi2d 
 |-  ( y = ( Re ` ( B / ( _i ^ k ) ) ) -> ( ( x e. A /\ 0 <_ y ) <-> ( x e. A /\ 0 <_ T ) ) )
8 7 5 ifbieq1d 
 |-  ( y = ( Re ` ( B / ( _i ^ k ) ) ) -> if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = if ( ( x e. A /\ 0 <_ T ) , T , 0 ) )
9 3 8 csbie 
 |-  [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = if ( ( x e. A /\ 0 <_ T ) , T , 0 )
10 9 mpteq2i 
 |-  ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) )
11 10 fveq2i 
 |-  ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) )
12 11 oveq2i 
 |-  ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) ) = ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) ) )
13 12 a1i 
 |-  ( k e. ( 0 ... 3 ) -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) ) = ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) ) ) )
14 13 sumeq2i 
 |-  sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) ) = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) ) )
15 2 14 eqtri 
 |-  S. A B _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) ) )