Metamath Proof Explorer


Theorem cbvitgv

Description: Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Hypothesis cbvitg.1
|- ( x = y -> B = C )
Assertion cbvitgv
|- S. A B _d x = S. A C _d y

Proof

Step Hyp Ref Expression
1 cbvitg.1
 |-  ( x = y -> B = C )
2 1 fvoveq1d
 |-  ( x = y -> ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) ) )
3 eleq1w
 |-  ( x = y -> ( x e. A <-> y e. A ) )
4 3 anbi1d
 |-  ( x = y -> ( ( x e. A /\ 0 <_ v ) <-> ( y e. A /\ 0 <_ v ) ) )
5 4 ifbid
 |-  ( x = y -> if ( ( x e. A /\ 0 <_ v ) , v , 0 ) = if ( ( y e. A /\ 0 <_ v ) , v , 0 ) )
6 2 5 csbeq12dv
 |-  ( x = y -> [_ ( Re ` ( B / ( _i ^ k ) ) ) / v ]_ if ( ( x e. A /\ 0 <_ v ) , v , 0 ) = [_ ( Re ` ( C / ( _i ^ k ) ) ) / v ]_ if ( ( y e. A /\ 0 <_ v ) , v , 0 ) )
7 6 cbvmptv
 |-  ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / v ]_ if ( ( x e. A /\ 0 <_ v ) , v , 0 ) ) = ( y e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / v ]_ if ( ( y e. A /\ 0 <_ v ) , v , 0 ) )
8 7 fveq2i
 |-  ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / v ]_ if ( ( x e. A /\ 0 <_ v ) , v , 0 ) ) ) = ( S.2 ` ( y e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / v ]_ if ( ( y e. A /\ 0 <_ v ) , v , 0 ) ) )
9 8 oveq2i
 |-  ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / v ]_ if ( ( x e. A /\ 0 <_ v ) , v , 0 ) ) ) ) = ( ( _i ^ k ) x. ( S.2 ` ( y e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / v ]_ if ( ( y e. A /\ 0 <_ v ) , v , 0 ) ) ) )
10 9 a1i
 |-  ( T. -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / v ]_ if ( ( x e. A /\ 0 <_ v ) , v , 0 ) ) ) ) = ( ( _i ^ k ) x. ( S.2 ` ( y e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / v ]_ if ( ( y e. A /\ 0 <_ v ) , v , 0 ) ) ) ) )
11 10 sumeq2sdv
 |-  ( T. -> sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / v ]_ if ( ( x e. A /\ 0 <_ v ) , v , 0 ) ) ) ) = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( y e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / v ]_ if ( ( y e. A /\ 0 <_ v ) , v , 0 ) ) ) ) )
12 11 mptru
 |-  sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / v ]_ if ( ( x e. A /\ 0 <_ v ) , v , 0 ) ) ) ) = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( y e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / v ]_ if ( ( y e. A /\ 0 <_ v ) , v , 0 ) ) ) )
13 df-itg
 |-  S. A B _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / v ]_ if ( ( x e. A /\ 0 <_ v ) , v , 0 ) ) ) )
14 df-itg
 |-  S. A C _d y = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( y e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / v ]_ if ( ( y e. A /\ 0 <_ v ) , v , 0 ) ) ) )
15 12 13 14 3eqtr4i
 |-  S. A B _d x = S. A C _d y