Metamath Proof Explorer

Theorem ditgeq2

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

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

Proof

Step Hyp Ref Expression
1 breq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐶 ≤ 𝐴 ↔ 𝐶 ≤ 𝐵 ) )
2 oveq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐶 (,) 𝐴 ) = ( 𝐶 (,) 𝐵 ) )
3 itgeq1 ⊢ ( ( 𝐶 (,) 𝐴 ) = ( 𝐶 (,) 𝐵 ) → ∫ ( 𝐶 (,) 𝐴 ) 𝐷 d 𝑥 = ∫ ( 𝐶 (,) 𝐵 ) 𝐷 d 𝑥 )
4 2 3 syl ⊢ ( 𝐴 = 𝐵 → ∫ ( 𝐶 (,) 𝐴 ) 𝐷 d 𝑥 = ∫ ( 𝐶 (,) 𝐵 ) 𝐷 d 𝑥 )
5 oveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 (,) 𝐶 ) = ( 𝐵 (,) 𝐶 ) )
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 𝑥 )