Theorem ditgeq2

Description: Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014)

	Ref	Expression
Assertion	ditgeq2	$$⊢A=B\to {\int }_C^{A}Ddx={\int }_C^{B}Ddx$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢A=B\to \left(C\le A\leftrightarrow C\le B\right)$$
2		oveq2	$$⊢A=B\to \left(C,A\right)=\left(C,B\right)$$
3		itgeq1	$$⊢\left(C,A\right)=\left(C,B\right)\to {\int }_{\left(C,A\right)}Ddx={\int }_{\left(C,B\right)}Ddx$$
4	2 3	syl	$$⊢A=B\to {\int }_{\left(C,A\right)}Ddx={\int }_{\left(C,B\right)}Ddx$$
5		oveq1	$$⊢A=B\to \left(A,C\right)=\left(B,C\right)$$
6		itgeq1	$$⊢\left(A,C\right)=\left(B,C\right)\to {\int }_{\left(A,C\right)}Ddx={\int }_{\left(B,C\right)}Ddx$$
7	5 6	syl	$$⊢A=B\to {\int }_{\left(A,C\right)}Ddx={\int }_{\left(B,C\right)}Ddx$$
8	7	negeqd	$$⊢A=B\to -{\int }_{\left(A,C\right)}Ddx=-{\int }_{\left(B,C\right)}Ddx$$
9	1 4 8	ifbieq12d	$$⊢A=B\to if\left(C\le A,{\int }_{\left(C,A\right)}Ddx,-{\int }_{\left(A,C\right)}Ddx\right)=if\left(C\le B,{\int }_{\left(C,B\right)}Ddx,-{\int }_{\left(B,C\right)}Ddx\right)$$
10		df-ditg	$$⊢{\int }_C^{A}Ddx=if\left(C\le A,{\int }_{\left(C,A\right)}Ddx,-{\int }_{\left(A,C\right)}Ddx\right)$$
11		df-ditg	$$⊢{\int }_C^{B}Ddx=if\left(C\le B,{\int }_{\left(C,B\right)}Ddx,-{\int }_{\left(B,C\right)}Ddx\right)$$
12	9 10 11	3eqtr4g	$$⊢A=B\to {\int }_C^{A}Ddx={\int }_C^{B}Ddx$$