# Metamath Proof Explorer

## Theorem ditgeq3d

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

Ref Expression
Hypotheses ditgeq3d.1 ${⊢}{\phi }\to {A}\le {B}$
ditgeq3d.2 ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {D}={E}$
Assertion ditgeq3d ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{D}d{x}={\int }_{{A}}^{{B}}{E}d{x}$

### Proof

Step Hyp Ref Expression
1 ditgeq3d.1 ${⊢}{\phi }\to {A}\le {B}$
2 ditgeq3d.2 ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {D}={E}$
3 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)$
4 1 iftrued ${⊢}{\phi }\to if\left({A}\le {B},{\int }_{\left({A},{B}\right)}{D}d{x},-{\int }_{\left({B},{A}\right)}{D}d{x}\right)={\int }_{\left({A},{B}\right)}{D}d{x}$
5 3 4 syl5eq ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{D}d{x}={\int }_{\left({A},{B}\right)}{D}d{x}$
6 2 itgeq2dv ${⊢}{\phi }\to {\int }_{\left({A},{B}\right)}{D}d{x}={\int }_{\left({A},{B}\right)}{E}d{x}$
7 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)$
8 1 iftrued ${⊢}{\phi }\to if\left({A}\le {B},{\int }_{\left({A},{B}\right)}{E}d{x},-{\int }_{\left({B},{A}\right)}{E}d{x}\right)={\int }_{\left({A},{B}\right)}{E}d{x}$
9 7 8 syl5req ${⊢}{\phi }\to {\int }_{\left({A},{B}\right)}{E}d{x}={\int }_{{A}}^{{B}}{E}d{x}$
10 5 6 9 3eqtrd ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{D}d{x}={\int }_{{A}}^{{B}}{E}d{x}$