Metamath Proof Explorer

Theorem itgeq12sdv

Description: Equality theorem for an integral. Deduction form. General version of itgeq1d and itgeq2sdv . (Contributed by GG, 1-Sep-2025)

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

Proof

Step Hyp Ref Expression
1 itgeq12sdv.1 
 |-  ( ph -> A = B )
2 itgeq12sdv.2 
 |-  ( ph -> C = D )
3 2 oveq1d 
 |-  ( ph -> ( C / ( _i ^ k ) ) = ( D / ( _i ^ k ) ) )
4 3 fveq2d 
 |-  ( ph -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( D / ( _i ^ k ) ) ) )
5 1 eleq2d 
 |-  ( ph -> ( x e. A <-> x e. B ) )
6 5 anbi1d 
 |-  ( ph -> ( ( x e. A /\ 0 <_ y ) <-> ( x e. B /\ 0 <_ y ) ) )
7 6 ifbid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = if ( ( x e. B /\ 0 <_ y ) , y , 0 ) )
8 4 7 csbeq12dv 
 |-  ( ph -> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = [_ ( Re ` ( D / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) )
9 8 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) = ( x e. RR |-> [_ ( Re ` ( D / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) )
10 9 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) = ( S.2 ` ( x e. RR |-> [_ ( Re ` ( D / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) ) )
11 10 oveq2d 
 |-  ( ph -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) ) = ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( D / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) ) ) )
12 11 sumeq2sdv 
 |-  ( ph -> sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) ) = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( D / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) ) ) )
13 df-itg 
 |-  S. A C _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) )
14 df-itg 
 |-  S. B D _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( D / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) ) )
15 12 13 14 3eqtr4g 
 |-  ( ph -> S. A C _d x = S. B D _d x )