This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⨜ [ 𝐴 → 𝐴 ] 𝐵 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