Theorem ditg0

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

	Ref	Expression
Assertion	ditg0	⊢ ⨜ [ 𝐴 → 𝐴 ] 𝐵 d 𝑥 = 0

Proof

Step	Hyp	Ref	Expression
1		df-ditg	⊢ ⨜ [ 𝐴 → 𝐴 ] 𝐵 d 𝑥 = if ( 𝐴 ≤ 𝐴 , ∫ ( 𝐴 (,) 𝐴 ) 𝐵 d 𝑥 , - ∫ ( 𝐴 (,) 𝐴 ) 𝐵 d 𝑥 )
2		iooid	⊢ ( 𝐴 (,) 𝐴 ) = ∅
3		itgeq1	⊢ ( ( 𝐴 (,) 𝐴 ) = ∅ → ∫ ( 𝐴 (,) 𝐴 ) 𝐵 d 𝑥 = ∫ ∅ 𝐵 d 𝑥 )
4	2 3	ax-mp	⊢ ∫ ( 𝐴 (,) 𝐴 ) 𝐵 d 𝑥 = ∫ ∅ 𝐵 d 𝑥
5		itg0	⊢ ∫ ∅ 𝐵 d 𝑥 = 0
6	4 5	eqtri	⊢ ∫ ( 𝐴 (,) 𝐴 ) 𝐵 d 𝑥 = 0
7	6	negeqi	⊢ - ∫ ( 𝐴 (,) 𝐴 ) 𝐵 d 𝑥 = - 0
8		neg0	⊢ - 0 = 0
9	7 8	eqtri	⊢ - ∫ ( 𝐴 (,) 𝐴 ) 𝐵 d 𝑥 = 0
10		ifeq12	⊢ ( ( ∫ ( 𝐴 (,) 𝐴 ) 𝐵 d 𝑥 = 0 ∧ - ∫ ( 𝐴 (,) 𝐴 ) 𝐵 d 𝑥 = 0 ) → if ( 𝐴 ≤ 𝐴 , ∫ ( 𝐴 (,) 𝐴 ) 𝐵 d 𝑥 , - ∫ ( 𝐴 (,) 𝐴 ) 𝐵 d 𝑥 ) = if ( 𝐴 ≤ 𝐴 , 0 , 0 ) )
11	6 9 10	mp2an	⊢ if ( 𝐴 ≤ 𝐴 , ∫ ( 𝐴 (,) 𝐴 ) 𝐵 d 𝑥 , - ∫ ( 𝐴 (,) 𝐴 ) 𝐵 d 𝑥 ) = if ( 𝐴 ≤ 𝐴 , 0 , 0 )
12		ifid	⊢ if ( 𝐴 ≤ 𝐴 , 0 , 0 ) = 0
13	11 12	eqtri	⊢ if ( 𝐴 ≤ 𝐴 , ∫ ( 𝐴 (,) 𝐴 ) 𝐵 d 𝑥 , - ∫ ( 𝐴 (,) 𝐴 ) 𝐵 d 𝑥 ) = 0
14	1 13	eqtri	⊢ ⨜ [ 𝐴 → 𝐴 ] 𝐵 d 𝑥 = 0