Metamath Proof Explorer

Theorem ditgeq1

Description: Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Assertion ditgeq1 
|- ( A = B -> S_ [ A -> C ] D _d x = S_ [ B -> C ] D _d x )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( A = B -> ( A <_ C <-> B <_ C ) )
2 oveq1 
 |-  ( A = B -> ( A (,) C ) = ( B (,) C ) )
3 itgeq1 
 |-  ( ( A (,) C ) = ( B (,) C ) -> S. ( A (,) C ) D _d x = S. ( B (,) C ) D _d x )
4 2 3 syl 
 |-  ( A = B -> S. ( A (,) C ) D _d x = S. ( B (,) C ) D _d x )
5 oveq2 
 |-  ( A = B -> ( C (,) A ) = ( C (,) B ) )
6 itgeq1 
 |-  ( ( C (,) A ) = ( C (,) B ) -> S. ( C (,) A ) D _d x = S. ( C (,) B ) D _d x )
7 5 6 syl 
 |-  ( A = B -> S. ( C (,) A ) D _d x = S. ( C (,) B ) D _d x )
8 7 negeqd 
 |-  ( A = B -> -u S. ( C (,) A ) D _d x = -u S. ( C (,) B ) D _d x )
9 1 4 8 ifbieq12d 
 |-  ( A = B -> if ( A <_ C , S. ( A (,) C ) D _d x , -u S. ( C (,) A ) D _d x ) = if ( B <_ C , S. ( B (,) C ) D _d x , -u S. ( C (,) B ) D _d x ) )
10 df-ditg 
 |-  S_ [ A -> C ] D _d x = if ( A <_ C , S. ( A (,) C ) D _d x , -u S. ( C (,) A ) D _d x )
11 df-ditg 
 |-  S_ [ B -> C ] D _d x = if ( B <_ C , S. ( B (,) C ) D _d x , -u S. ( C (,) B ) D _d x )
12 9 10 11 3eqtr4g 
 |-  ( A = B -> S_ [ A -> C ] D _d x = S_ [ B -> C ] D _d x )