Metamath Proof Explorer

Theorem ditgeq3

Description: Equality theorem for the directed integral. (The domain of the equality here is very rough; for more precise bounds one should decompose it with ditgpos first and use the equality theorems for df-itg .) (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Assertion ditgeq3 ⊢ ∀ x ∈ ℝ D = E → ∫ A B D dx = ∫ A B E dx

Proof

Step Hyp Ref Expression
1 ioossre ⊢ A B ⊆ ℝ
2 ssralv ⊢ A B ⊆ ℝ → ∀ x ∈ ℝ D = E → ∀ x ∈ A B D = E
3 1 2 ax-mp ⊢ ∀ x ∈ ℝ D = E → ∀ x ∈ A B D = E
4 itgeq2 ⊢ ∀ x ∈ A B D = E → ∫ A B D dx = ∫ A B E dx
5 3 4 syl ⊢ ∀ x ∈ ℝ D = E → ∫ A B D dx = ∫ A B E dx
6 ioossre ⊢ B A ⊆ ℝ
7 ssralv ⊢ B A ⊆ ℝ → ∀ x ∈ ℝ D = E → ∀ x ∈ B A D = E
8 6 7 ax-mp ⊢ ∀ x ∈ ℝ D = E → ∀ x ∈ B A D = E
9 itgeq2 ⊢ ∀ x ∈ B A D = E → ∫ B A D dx = ∫ B A E dx
10 8 9 syl ⊢ ∀ x ∈ ℝ D = E → ∫ B A D dx = ∫ B A E dx
11 10 negeqd ⊢ ∀ x ∈ ℝ D = E → − ∫ B A D dx = − ∫ B A E dx
12 5 11 ifeq12d ⊢ ∀ x ∈ ℝ D = E → if A ≤ B ∫ A B D dx − ∫ B A D dx = if A ≤ B ∫ A B E dx − ∫ B A E dx
13 df-ditg ⊢ ∫ A B D dx = if A ≤ B ∫ A B D dx − ∫ B A D dx
14 df-ditg ⊢ ∫ A B E dx = if A ≤ B ∫ A B E dx − ∫ B A E dx
15 12 13 14 3eqtr4g ⊢ ∀ x ∈ ℝ D = E → ∫ A B D dx = ∫ A B E dx