Metamath Proof Explorer

Theorem itgeq12dv

Description: Equality theorem for an integral. (Contributed by Thierry Arnoux, 14-Feb-2017)

Ref Expression
Hypotheses itgeq12dv.2 
|- ( ph -> A = B )
itgeq12dv.1 
|- ( ( ph /\ x e. A ) -> C = D )
Assertion itgeq12dv 
|- ( ph -> S. A C _d x = S. B D _d x )

Proof

Step Hyp Ref Expression
1 itgeq12dv.2 
 |-  ( ph -> A = B )
2 itgeq12dv.1 
 |-  ( ( ph /\ x e. A ) -> C = D )
3 2 fvoveq1d 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( D / ( _i ^ k ) ) ) )
4 3 breq2d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) <-> 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) )
5 4 pm5.32da 
 |-  ( ph -> ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) <-> ( x e. A /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) ) )
6 1 eleq2d 
 |-  ( ph -> ( x e. A <-> x e. B ) )
7 6 anbi1d 
 |-  ( ph -> ( ( x e. A /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) <-> ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) ) )
8 5 7 bitrd 
 |-  ( ph -> ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) <-> ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) ) )
9 3 adantrr 
 |-  ( ( ph /\ ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) ) -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( D / ( _i ^ k ) ) ) )
10 eqidd 
 |-  ( ( ph /\ -. ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) ) -> 0 = 0 )
11 8 9 10 ifbieq12d2 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) )
12 11 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) )
13 12 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ) )
14 13 oveq2d 
 |-  ( ph -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ) ) )
15 14 sumeq2sdv 
 |-  ( ph -> sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ) ) )
16 eqid 
 |-  ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) )
17 16 dfitg 
 |-  S. A C _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
18 eqid 
 |-  ( Re ` ( D / ( _i ^ k ) ) ) = ( Re ` ( D / ( _i ^ k ) ) )
19 18 dfitg 
 |-  S. B D _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( D / ( _i ^ k ) ) ) ) , ( Re ` ( D / ( _i ^ k ) ) ) , 0 ) ) ) )
20 15 17 19 3eqtr4g 
 |-  ( ph -> S. A C _d x = S. B D _d x )