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 𝑥 )