Metamath Proof Explorer

Theorem cbvitg

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

Ref Expression
Hypotheses cbvitg.1 
|- ( x = y -> B = C )
cbvitg.2 
|- F/_ y B
cbvitg.3 
|- F/_ x C
Assertion cbvitg 
|- S. A B _d x = S. A C _d y

Proof

Step Hyp Ref Expression
1 cbvitg.1 
 |-  ( x = y -> B = C )
2 cbvitg.2 
 |-  F/_ y B
3 cbvitg.3 
 |-  F/_ x C
4 nfv 
 |-  F/ y x e. A
5 nfcv 
 |-  F/_ y 0
6 nfcv 
 |-  F/_ y <_
7 nfcv 
 |-  F/_ y Re
8 nfcv 
 |-  F/_ y /
9 nfcv 
 |-  F/_ y ( _i ^ k )
10 2 8 9 nfov 
 |-  F/_ y ( B / ( _i ^ k ) )
11 7 10 nffv 
 |-  F/_ y ( Re ` ( B / ( _i ^ k ) ) )
12 5 6 11 nfbr 
 |-  F/ y 0 <_ ( Re ` ( B / ( _i ^ k ) ) )
13 4 12 nfan 
 |-  F/ y ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) )
14 13 11 5 nfif 
 |-  F/_ y if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 )
15 nfv 
 |-  F/ x y e. A
16 nfcv 
 |-  F/_ x 0
17 nfcv 
 |-  F/_ x <_
18 nfcv 
 |-  F/_ x Re
19 nfcv 
 |-  F/_ x /
20 nfcv 
 |-  F/_ x ( _i ^ k )
21 3 19 20 nfov 
 |-  F/_ x ( C / ( _i ^ k ) )
22 18 21 nffv 
 |-  F/_ x ( Re ` ( C / ( _i ^ k ) ) )
23 16 17 22 nfbr 
 |-  F/ x 0 <_ ( Re ` ( C / ( _i ^ k ) ) )
24 15 23 nfan 
 |-  F/ x ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) )
25 24 22 16 nfif 
 |-  F/_ x if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 )
26 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
27 1 fvoveq1d 
 |-  ( x = y -> ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) ) )
28 27 breq2d 
 |-  ( x = y -> ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) <-> 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) )
29 26 28 anbi12d 
 |-  ( x = y -> ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) <-> ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) ) )
30 29 27 ifbieq1d 
 |-  ( x = y -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) = if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
31 14 25 30 cbvmpt 
 |-  ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( y e. RR |-> if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
32 31 a1i 
 |-  ( k e. ( 0 ... 3 ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( y e. RR |-> if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
33 32 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 ` ( y e. RR |-> if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
34 33 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 ` ( y e. RR |-> if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) )
35 34 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 ` ( y e. RR |-> if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
36 eqid 
 |-  ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) )
37 36 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 ) ) ) )
38 eqid 
 |-  ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) )
39 38 dfitg 
 |-  S. A C _d y = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( y e. RR |-> if ( ( y e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
40 35 37 39 3eqtr4i 
 |-  S. A B _d x = S. A C _d y