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 syl6bi
 |-  ( 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 syl5eq
 |-  ( -. 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 )