Metamath Proof Explorer

Theorem itgeq12i

Description: Equality inference for an integral. General version of itgeq1i and itgeq2i . (Contributed by GG, 1-Sep-2025)

Ref Expression
Hypotheses itgeq12i.1 
|- A = B
itgeq12i.2 
|- C = D
Assertion itgeq12i 
|- S. A C _d x = S. B D _d x

Proof

Step Hyp Ref Expression
1 itgeq12i.1 
 |-  A = B
2 itgeq12i.2 
 |-  C = D
3 2 oveq1i 
 |-  ( C / ( _i ^ k ) ) = ( D / ( _i ^ k ) )
4 3 fveq2i 
 |-  ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( D / ( _i ^ k ) ) )
5 1 eleq2i 
 |-  ( x e. A <-> x e. B )
6 5 anbi1i 
 |-  ( ( x e. A /\ 0 <_ y ) <-> ( x e. B /\ 0 <_ y ) )
7 ifbi 
 |-  ( ( ( x e. A /\ 0 <_ y ) <-> ( x e. B /\ 0 <_ y ) ) -> if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = if ( ( x e. B /\ 0 <_ y ) , y , 0 ) )
8 6 7 ax-mp 
 |-  if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = if ( ( x e. B /\ 0 <_ y ) , y , 0 )
9 8 ax-gen 
 |-  A. y if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = if ( ( x e. B /\ 0 <_ y ) , y , 0 )
10 4 9 pm3.2i 
 |-  ( ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( D / ( _i ^ k ) ) ) /\ A. y if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = if ( ( x e. B /\ 0 <_ y ) , y , 0 ) )
11 csbeq2 
 |-  ( A. y if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = if ( ( x e. B /\ 0 <_ y ) , y , 0 ) -> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) )
12 csbeq1 
 |-  ( ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( D / ( _i ^ k ) ) ) -> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) = [_ ( Re ` ( D / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) )
13 11 12 sylan9eqr 
 |-  ( ( ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( D / ( _i ^ k ) ) ) /\ A. y if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) -> [_ ( 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 ) )
14 10 13 ax-mp 
 |-  [_ ( 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 )
15 14 mpteq2i 
 |-  ( 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 ) )
16 15 fveq2i 
 |-  ( 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 ) ) )
17 16 oveq2i 
 |-  ( ( _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 ) ) ) )
18 17 sumeq2si 
 |-  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 ) ) ) )
19 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 ) ) ) )
20 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 ) ) ) )
21 18 19 20 3eqtr4i 
 |-  S. A C _d x = S. B D _d x