Metamath Proof Explorer

Theorem cbvditgvw2

Description: Change bound variable and domain in a directed integral, using implicit substitution. (Contributed by GG, 1-Sep-2025)

Ref Expression
Hypotheses cbvditgvw2.1 
|- A = B
cbvditgvw2.2 
|- C = D
cbvditgvw2.3 
|- ( x = y -> E = F )
Assertion cbvditgvw2 
|- S_ [ A -> C ] E _d x = S_ [ B -> D ] F _d y

Proof

Step Hyp Ref Expression
1 cbvditgvw2.1 
 |-  A = B
2 cbvditgvw2.2 
 |-  C = D
3 cbvditgvw2.3 
 |-  ( x = y -> E = F )
4 1 2 breq12i 
 |-  ( A <_ C <-> B <_ D )
5 1 2 oveq12i 
 |-  ( A (,) C ) = ( B (,) D )
6 5 a1i 
 |-  ( x = y -> ( A (,) C ) = ( B (,) D ) )
7 3 6 cbvitgvw2 
 |-  S. ( A (,) C ) E _d x = S. ( B (,) D ) F _d y
8 2 a1i 
 |-  ( x = y -> C = D )
9 1 a1i 
 |-  ( x = y -> A = B )
10 8 9 oveq12d 
 |-  ( x = y -> ( C (,) A ) = ( D (,) B ) )
11 3 10 cbvitgvw2 
 |-  S. ( C (,) A ) E _d x = S. ( D (,) B ) F _d y
12 11 negeqi 
 |-  -u S. ( C (,) A ) E _d x = -u S. ( D (,) B ) F _d y
13 4 7 12 ifbieq12i 
 |-  if ( A <_ C , S. ( A (,) C ) E _d x , -u S. ( C (,) A ) E _d x ) = if ( B <_ D , S. ( B (,) D ) F _d y , -u S. ( D (,) B ) F _d y )
14 df-ditg 
 |-  S_ [ A -> C ] E _d x = if ( A <_ C , S. ( A (,) C ) E _d x , -u S. ( C (,) A ) E _d x )
15 df-ditg 
 |-  S_ [ B -> D ] F _d y = if ( B <_ D , S. ( B (,) D ) F _d y , -u S. ( D (,) B ) F _d y )
16 13 14 15 3eqtr4i 
 |-  S_ [ A -> C ] E _d x = S_ [ B -> D ] F _d y