Metamath Proof Explorer

Theorem itgvallem

Description: Substitution lemma. (Contributed by Mario Carneiro, 7-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypothesis itgvallem.1 
|- ( _i ^ K ) = T
Assertion itgvallem 
|- ( k = K -> ( 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 ` ( B / T ) ) ) , ( Re ` ( B / T ) ) , 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 itgvallem.1 
 |-  ( _i ^ K ) = T
2 oveq2 
 |-  ( k = K -> ( _i ^ k ) = ( _i ^ K ) )
3 2 1 eqtrdi 
 |-  ( k = K -> ( _i ^ k ) = T )
4 3 oveq2d 
 |-  ( k = K -> ( B / ( _i ^ k ) ) = ( B / T ) )
5 4 fveq2d 
 |-  ( k = K -> ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / T ) ) )
6 5 breq2d 
 |-  ( k = K -> ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) <-> 0 <_ ( Re ` ( B / T ) ) ) )
7 6 anbi2d 
 |-  ( k = K -> ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) <-> ( x e. A /\ 0 <_ ( Re ` ( B / T ) ) ) ) )
8 7 5 ifbieq1d 
 |-  ( k = K -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( B / T ) ) ) , ( Re ` ( B / T ) ) , 0 ) )
9 8 mpteq2dv 
 |-  ( k = K -> ( 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 ` ( B / T ) ) ) , ( Re ` ( B / T ) ) , 0 ) ) )
10 9 fveq2d 
 |-  ( k = K -> ( 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 ` ( B / T ) ) ) , ( Re ` ( B / T ) ) , 0 ) ) ) )