Metamath Proof Explorer

Theorem ditgneg

Description: Value of the directed integral in the backward direction. (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Hypotheses ditgpos.1 
|- ( ph -> A <_ B )
ditgneg.2 
|- ( ph -> A e. RR )
ditgneg.3 
|- ( ph -> B e. RR )
Assertion ditgneg 
|- ( ph -> S_ [ B -> A ] C _d x = -u S. ( A (,) B ) C _d x )

Proof

Step Hyp Ref Expression
1 ditgpos.1 
 |-  ( ph -> A <_ B )
2 ditgneg.2 
 |-  ( ph -> A e. RR )
3 ditgneg.3 
 |-  ( ph -> B e. RR )
4 1 biantrurd 
 |-  ( ph -> ( B <_ A <-> ( A <_ B /\ B <_ A ) ) )
5 2 3 letri3d 
 |-  ( ph -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
6 4 5 bitr4d 
 |-  ( ph -> ( B <_ A <-> A = B ) )
7 ditg0 
 |-  S_ [ B -> B ] C _d x = 0
8 neg0 
 |-  -u 0 = 0
9 7 8 eqtr4i 
 |-  S_ [ B -> B ] C _d x = -u 0
10 ditgeq2 
 |-  ( A = B -> S_ [ B -> A ] C _d x = S_ [ B -> B ] C _d x )
11 oveq1 
 |-  ( A = B -> ( A (,) B ) = ( B (,) B ) )
12 iooid 
 |-  ( B (,) B ) = (/)
13 11 12 eqtrdi 
 |-  ( A = B -> ( A (,) B ) = (/) )
14 itgeq1 
 |-  ( ( A (,) B ) = (/) -> S. ( A (,) B ) C _d x = S. (/) C _d x )
15 13 14 syl 
 |-  ( A = B -> S. ( A (,) B ) C _d x = S. (/) C _d x )
16 itg0 
 |-  S. (/) C _d x = 0
17 15 16 eqtrdi 
 |-  ( A = B -> S. ( A (,) B ) C _d x = 0 )
18 17 negeqd 
 |-  ( A = B -> -u S. ( A (,) B ) C _d x = -u 0 )
19 9 10 18 3eqtr4a 
 |-  ( A = B -> S_ [ B -> A ] C _d x = -u S. ( A (,) B ) C _d x )
20 6 19 biimtrdi 
 |-  ( ph -> ( B <_ A -> S_ [ B -> A ] C _d x = -u S. ( A (,) B ) C _d x ) )
21 df-ditg 
 |-  S_ [ B -> A ] C _d x = if ( B <_ A , S. ( B (,) A ) C _d x , -u S. ( A (,) B ) C _d x )
22 iffalse 
 |-  ( -. B <_ A -> if ( B <_ A , S. ( B (,) A ) C _d x , -u S. ( A (,) B ) C _d x ) = -u S. ( A (,) B ) C _d x )
23 21 22 eqtrid 
 |-  ( -. B <_ A -> S_ [ B -> A ] C _d x = -u S. ( A (,) B ) C _d x )
24 20 23 pm2.61d1 
 |-  ( ph -> S_ [ B -> A ] C _d x = -u S. ( A (,) B ) C _d x )