# 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 ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{D}={E}\to {\int }_{{A}}^{{B}}{D}d{x}={\int }_{{A}}^{{B}}{E}d{x}$

### Proof

Step Hyp Ref Expression
1 ioossre ${⊢}\left({A},{B}\right)\subseteq ℝ$
2 ssralv ${⊢}\left({A},{B}\right)\subseteq ℝ\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{D}={E}\to \forall {x}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}{D}={E}\right)$
3 1 2 ax-mp ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{D}={E}\to \forall {x}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}{D}={E}$
4 itgeq2 ${⊢}\forall {x}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}{D}={E}\to {\int }_{\left({A},{B}\right)}{D}d{x}={\int }_{\left({A},{B}\right)}{E}d{x}$
5 3 4 syl ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{D}={E}\to {\int }_{\left({A},{B}\right)}{D}d{x}={\int }_{\left({A},{B}\right)}{E}d{x}$
6 ioossre ${⊢}\left({B},{A}\right)\subseteq ℝ$
7 ssralv ${⊢}\left({B},{A}\right)\subseteq ℝ\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{D}={E}\to \forall {x}\in \left({B},{A}\right)\phantom{\rule{.4em}{0ex}}{D}={E}\right)$
8 6 7 ax-mp ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{D}={E}\to \forall {x}\in \left({B},{A}\right)\phantom{\rule{.4em}{0ex}}{D}={E}$
9 itgeq2 ${⊢}\forall {x}\in \left({B},{A}\right)\phantom{\rule{.4em}{0ex}}{D}={E}\to {\int }_{\left({B},{A}\right)}{D}d{x}={\int }_{\left({B},{A}\right)}{E}d{x}$
10 8 9 syl ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{D}={E}\to {\int }_{\left({B},{A}\right)}{D}d{x}={\int }_{\left({B},{A}\right)}{E}d{x}$
11 10 negeqd ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{D}={E}\to -{\int }_{\left({B},{A}\right)}{D}d{x}=-{\int }_{\left({B},{A}\right)}{E}d{x}$
12 5 11 ifeq12d ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{D}={E}\to if\left({A}\le {B},{\int }_{\left({A},{B}\right)}{D}d{x},-{\int }_{\left({B},{A}\right)}{D}d{x}\right)=if\left({A}\le {B},{\int }_{\left({A},{B}\right)}{E}d{x},-{\int }_{\left({B},{A}\right)}{E}d{x}\right)$
13 df-ditg ${⊢}{\int }_{{A}}^{{B}}{D}d{x}=if\left({A}\le {B},{\int }_{\left({A},{B}\right)}{D}d{x},-{\int }_{\left({B},{A}\right)}{D}d{x}\right)$
14 df-ditg ${⊢}{\int }_{{A}}^{{B}}{E}d{x}=if\left({A}\le {B},{\int }_{\left({A},{B}\right)}{E}d{x},-{\int }_{\left({B},{A}\right)}{E}d{x}\right)$
15 12 13 14 3eqtr4g ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{D}={E}\to {\int }_{{A}}^{{B}}{D}d{x}={\int }_{{A}}^{{B}}{E}d{x}$