Theorem ditgeq123i

Description: Equality inference for the directed integral. General version of ditgeq12i and ditgeq3i . (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	ditgeq123i.1	$$⊢A=B$$
	ditgeq123i.2	$$⊢C=D$$
	ditgeq123i.3	$$⊢E=F$$
Assertion	ditgeq123i	$$⊢{\int }_A^{C}Edx={\int }_B^{D}Fdx$$

Proof

Step	Hyp	Ref	Expression
1		ditgeq123i.1	$$⊢A=B$$
2		ditgeq123i.2	$$⊢C=D$$
3		ditgeq123i.3	$$⊢E=F$$
4	1 2	breq12i	$$⊢A\le C\leftrightarrow B\le D$$
5	1 2	oveq12i	$$⊢\left(A,C\right)=\left(B,D\right)$$
6	5 3	itgeq12i	$$⊢{\int }_{\left(A,C\right)}Edx={\int }_{\left(B,D\right)}Fdx$$
7	2 1	oveq12i	$$⊢\left(C,A\right)=\left(D,B\right)$$
8	7 3	itgeq12i	$$⊢{\int }_{\left(C,A\right)}Edx={\int }_{\left(D,B\right)}Fdx$$
9	8	negeqi	$$⊢-{\int }_{\left(C,A\right)}Edx=-{\int }_{\left(D,B\right)}Fdx$$
10	4 6 9	ifbieq12i	$$⊢if\left(A\le C,{\int }_{\left(A,C\right)}Edx,-{\int }_{\left(C,A\right)}Edx\right)=if\left(B\le D,{\int }_{\left(B,D\right)}Fdx,-{\int }_{\left(D,B\right)}Fdx\right)$$
11		df-ditg	$$⊢{\int }_A^{C}Edx=if\left(A\le C,{\int }_{\left(A,C\right)}Edx,-{\int }_{\left(C,A\right)}Edx\right)$$
12		df-ditg	$$⊢{\int }_B^{D}Fdx=if\left(B\le D,{\int }_{\left(B,D\right)}Fdx,-{\int }_{\left(D,B\right)}Fdx\right)$$
13	10 11 12	3eqtr4i	$$⊢{\int }_A^{C}Edx={\int }_B^{D}Fdx$$