Metamath Proof Explorer

Theorem ditgeq1

Description: Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Assertion ditgeq1 ( 𝐴 = 𝐵 → ⨜ [ 𝐴 → 𝐶 ] 𝐷 d 𝑥 = ⨜ [ 𝐵 → 𝐶 ] 𝐷 d 𝑥 )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ≤ 𝐶 ↔ 𝐵 ≤ 𝐶 ) )
2 oveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 (,) 𝐶 ) = ( 𝐵 (,) 𝐶 ) )
3 itgeq1 ⊢ ( ( 𝐴 (,) 𝐶 ) = ( 𝐵 (,) 𝐶 ) → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 )
4 2 3 syl ⊢ ( 𝐴 = 𝐵 → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 )
5 oveq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐶 (,) 𝐴 ) = ( 𝐶 (,) 𝐵 ) )
6 itgeq1 ⊢ ( ( 𝐶 (,) 𝐴 ) = ( 𝐶 (,) 𝐵 ) → ∫ ( 𝐶 (,) 𝐴 ) 𝐷 d 𝑥 = ∫ ( 𝐶 (,) 𝐵 ) 𝐷 d 𝑥 )
7 5 6 syl ⊢ ( 𝐴 = 𝐵 → ∫ ( 𝐶 (,) 𝐴 ) 𝐷 d 𝑥 = ∫ ( 𝐶 (,) 𝐵 ) 𝐷 d 𝑥 )
8 7 negeqd ⊢ ( 𝐴 = 𝐵 → - ∫ ( 𝐶 (,) 𝐴 ) 𝐷 d 𝑥 = - ∫ ( 𝐶 (,) 𝐵 ) 𝐷 d 𝑥 )
9 1 4 8 ifbieq12d ⊢ ( 𝐴 = 𝐵 → if ( 𝐴 ≤ 𝐶 , ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 , - ∫ ( 𝐶 (,) 𝐴 ) 𝐷 d 𝑥 ) = if ( 𝐵 ≤ 𝐶 , ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 , - ∫ ( 𝐶 (,) 𝐵 ) 𝐷 d 𝑥 ) )
10 df-ditg ⊢ ⨜ [ 𝐴 → 𝐶 ] 𝐷 d 𝑥 = if ( 𝐴 ≤ 𝐶 , ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 , - ∫ ( 𝐶 (,) 𝐴 ) 𝐷 d 𝑥 )
11 df-ditg ⊢ ⨜ [ 𝐵 → 𝐶 ] 𝐷 d 𝑥 = if ( 𝐵 ≤ 𝐶 , ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 , - ∫ ( 𝐶 (,) 𝐵 ) 𝐷 d 𝑥 )
12 9 10 11 3eqtr4g ⊢ ( 𝐴 = 𝐵 → ⨜ [ 𝐴 → 𝐶 ] 𝐷 d 𝑥 = ⨜ [ 𝐵 → 𝐶 ] 𝐷 d 𝑥 )