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}Ddx={\int }_A^{B}Edx$$

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}Ddx=if\left(A\le B,{\int }_{\left(A,B\right)}Ddx,-{\int }_{\left(B,A\right)}Ddx\right)$$
4	1	iftrued	$$⊢\phi \to if\left(A\le B,{\int }_{\left(A,B\right)}Ddx,-{\int }_{\left(B,A\right)}Ddx\right)={\int }_{\left(A,B\right)}Ddx$$
5	3 4	syl5eq	$$⊢\phi \to {\int }_A^{B}Ddx={\int }_{\left(A,B\right)}Ddx$$
6	2	itgeq2dv	$$⊢\phi \to {\int }_{\left(A,B\right)}Ddx={\int }_{\left(A,B\right)}Edx$$
7		df-ditg	$$⊢{\int }_A^{B}Edx=if\left(A\le B,{\int }_{\left(A,B\right)}Edx,-{\int }_{\left(B,A\right)}Edx\right)$$
8	1	iftrued	$$⊢\phi \to if\left(A\le B,{\int }_{\left(A,B\right)}Edx,-{\int }_{\left(B,A\right)}Edx\right)={\int }_{\left(A,B\right)}Edx$$
9	7 8	syl5req	$$⊢\phi \to {\int }_{\left(A,B\right)}Edx={\int }_A^{B}Edx$$
10	5 6 9	3eqtrd	$$⊢\phi \to {\int }_A^{B}Ddx={\int }_A^{B}Edx$$