This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ditgeq3d

Description: Equality theorem for the directed integral. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ditgeq3d.1 ⊢ φ → A ≤ B
ditgeq3d.2 ⊢ φ ∧ x ∈ A B → D = E
Assertion ditgeq3d ⊢ φ → ∫ A B D dx = ∫ A B E dx

Proof

Step Hyp Ref Expression
1 ditgeq3d.1 ⊢ φ → A ≤ B
2 ditgeq3d.2 ⊢ φ ∧ x ∈ A B → D = E
3 df-ditg ⊢ ∫ A B D dx = if A ≤ B ∫ A B D dx − ∫ B A D dx
4 1 iftrued ⊢ φ → if A ≤ B ∫ A B D dx − ∫ B A D dx = ∫ A B D dx
5 3 4 eqtrid ⊢ φ → ∫ A B D dx = ∫ A B D dx
6 2 itgeq2dv ⊢ φ → ∫ A B D dx = ∫ A B E dx
7 df-ditg ⊢ ∫ A B E dx = if A ≤ B ∫ A B E dx − ∫ B A E dx
8 1 iftrued ⊢ φ → if A ≤ B ∫ A B E dx − ∫ B A E dx = ∫ A B E dx
9 7 8 eqtr2id ⊢ φ → ∫ A B E dx = ∫ A B E dx
10 5 6 9 3eqtrd ⊢ φ → ∫ A B D dx = ∫ A B E dx