Metamath Proof Explorer

Theorem ditg0

Description: Value of the directed integral from a point to itself. (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Assertion ditg0 
|- S_ [ A -> A ] B _d x = 0

Proof

Step Hyp Ref Expression
1 df-ditg 
 |-  S_ [ A -> A ] B _d x = if ( A <_ A , S. ( A (,) A ) B _d x , -u S. ( A (,) A ) B _d x )
2 iooid 
 |-  ( A (,) A ) = (/)
3 itgeq1 
 |-  ( ( A (,) A ) = (/) -> S. ( A (,) A ) B _d x = S. (/) B _d x )
4 2 3 ax-mp 
 |-  S. ( A (,) A ) B _d x = S. (/) B _d x
5 itg0 
 |-  S. (/) B _d x = 0
6 4 5 eqtri 
 |-  S. ( A (,) A ) B _d x = 0
7 6 negeqi 
 |-  -u S. ( A (,) A ) B _d x = -u 0
8 neg0 
 |-  -u 0 = 0
9 7 8 eqtri 
 |-  -u S. ( A (,) A ) B _d x = 0
10 ifeq12 
 |-  ( ( S. ( A (,) A ) B _d x = 0 /\ -u S. ( A (,) A ) B _d x = 0 ) -> if ( A <_ A , S. ( A (,) A ) B _d x , -u S. ( A (,) A ) B _d x ) = if ( A <_ A , 0 , 0 ) )
11 6 9 10 mp2an 
 |-  if ( A <_ A , S. ( A (,) A ) B _d x , -u S. ( A (,) A ) B _d x ) = if ( A <_ A , 0 , 0 )
12 ifid 
 |-  if ( A <_ A , 0 , 0 ) = 0
13 11 12 eqtri 
 |-  if ( A <_ A , S. ( A (,) A ) B _d x , -u S. ( A (,) A ) B _d x ) = 0
14 1 13 eqtri 
 |-  S_ [ A -> A ] B _d x = 0