This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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