Metamath Proof Explorer

Theorem cbvitgdavw2

Description: Change bound variable and domain in an integral. Deduction form. (Contributed by GG, 14-Aug-2025)

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

Proof

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