Metamath Proof Explorer

Theorem ditgeq2

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

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

Proof

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