Metamath Proof Explorer

Theorem ditgeq1

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

Ref Expression
Assertion ditgeq1 ⊢ A = B → ∫ A C D dx = ∫ B C D dx

Proof

Step Hyp Ref Expression
1 breq1 ⊢ A = B → A ≤ C ↔ B ≤ C
2 oveq1 ⊢ A = B → A C = B C
3 itgeq1 ⊢ A C = B C → ∫ A C D dx = ∫ B C D dx
4 2 3 syl ⊢ A = B → ∫ A C D dx = ∫ B C D dx
5 oveq2 ⊢ A = B → C A = C B
6 itgeq1 ⊢ C A = C B → ∫ C A D dx = ∫ C B D dx
7 5 6 syl ⊢ A = B → ∫ C A D dx = ∫ C B D dx
8 7 negeqd ⊢ A = B → − ∫ C A D dx = − ∫ C B D dx
9 1 4 8 ifbieq12d ⊢ A = B → if A ≤ C ∫ A C D dx − ∫ C A D dx = if B ≤ C ∫ B C D dx − ∫ C B D dx
10 df-ditg ⊢ ∫ A C D dx = if A ≤ C ∫ A C D dx − ∫ C A D dx
11 df-ditg ⊢ ∫ B C D dx = if B ≤ C ∫ B C D dx − ∫ C B D dx
12 9 10 11 3eqtr4g ⊢ A = B → ∫ A C D dx = ∫ B C D dx