Metamath Proof Explorer


Theorem cbvditg

Description: Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 cbvditg.1
 |-  ( x = y -> C = D )
2 cbvditg.2
 |-  F/_ y C
3 cbvditg.3
 |-  F/_ x D
4 biid
 |-  ( A <_ B <-> A <_ B )
5 1 2 3 cbvitg
 |-  S. ( A (,) B ) C _d x = S. ( A (,) B ) D _d y
6 1 2 3 cbvitg
 |-  S. ( B (,) A ) C _d x = S. ( B (,) A ) D _d y
7 6 negeqi
 |-  -u S. ( B (,) A ) C _d x = -u S. ( B (,) A ) D _d y
8 4 5 7 ifbieq12i
 |-  if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x ) = if ( A <_ B , S. ( A (,) B ) D _d y , -u S. ( B (,) A ) D _d y )
9 df-ditg
 |-  S_ [ A -> B ] C _d x = if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x )
10 df-ditg
 |-  S_ [ A -> B ] D _d y = if ( A <_ B , S. ( A (,) B ) D _d y , -u S. ( B (,) A ) D _d y )
11 8 9 10 3eqtr4i
 |-  S_ [ A -> B ] C _d x = S_ [ A -> B ] D _d y