Theorem cbvditgvw2

Description: Change bound variable and domain in a directed integral, using implicit substitution. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	cbvditgvw2.1	$$⊢A=B$$
	cbvditgvw2.2	$$⊢C=D$$
	cbvditgvw2.3	$$⊢x=y\to E=F$$
Assertion	cbvditgvw2	$$⊢{\int }_A^{C}Edx={\int }_B^{D}Fdy$$

Proof

Step	Hyp	Ref	Expression
1		cbvditgvw2.1	$$⊢A=B$$
2		cbvditgvw2.2	$$⊢C=D$$
3		cbvditgvw2.3	$$⊢x=y\to 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	a1i	$$⊢x=y\to \left(A,C\right)=\left(B,D\right)$$
7	3 6	cbvitgvw2	$$⊢{\int }_{\left(A,C\right)}Edx={\int }_{\left(B,D\right)}Fdy$$
8	2	a1i	$$⊢x=y\to C=D$$
9	1	a1i	$$⊢x=y\to A=B$$
10	8 9	oveq12d	$$⊢x=y\to \left(C,A\right)=\left(D,B\right)$$
11	3 10	cbvitgvw2	$$⊢{\int }_{\left(C,A\right)}Edx={\int }_{\left(D,B\right)}Fdy$$
12	11	negeqi	$$⊢-{\int }_{\left(C,A\right)}Edx=-{\int }_{\left(D,B\right)}Fdy$$
13	4 7 12	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)}Fdy,-{\int }_{\left(D,B\right)}Fdy\right)$$
14		df-ditg	$$⊢{\int }_A^{C}Edx=if\left(A\le C,{\int }_{\left(A,C\right)}Edx,-{\int }_{\left(C,A\right)}Edx\right)$$
15		df-ditg	$$⊢{\int }_B^{D}Fdy=if\left(B\le D,{\int }_{\left(B,D\right)}Fdy,-{\int }_{\left(D,B\right)}Fdy\right)$$
16	13 14 15	3eqtr4i	$$⊢{\int }_A^{C}Edx={\int }_B^{D}Fdy$$