Metamath Proof Explorer

Theorem ditgeq2

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

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

Proof

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