Theorem cbvitgvw2

Description: Change bound variable and domain in an integral, using implicit substitution. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypotheses	cbvitgvw2.1	$$⊢x=y\to C=D$$
	cbvitgvw2.2	$$⊢x=y\to A=B$$
Assertion	cbvitgvw2	$$⊢{\int }_{A}Cdx={\int }_{B}Ddy$$

Proof

Step	Hyp	Ref	Expression
1		cbvitgvw2.1	$$⊢x=y\to C=D$$
2		cbvitgvw2.2	$$⊢x=y\to A=B$$
3	1	fvoveq1d	$$⊢x=y\to \Re \left(\frac{C}{{\mathrm{i}}^t}\right)=\Re \left(\frac{D}{{\mathrm{i}}^t}\right)$$
4		id	$$⊢x=y\to x=y$$
5	4 2	eleq12d	$$⊢x=y\to \left(x\in A\leftrightarrow y\in B\right)$$
6	5	anbi1d	$$⊢x=y\to \left(\left(x\in A\wedge 0\le v\right)\leftrightarrow \left(y\in B\wedge 0\le v\right)\right)$$
7	6	ifbid	$$⊢x=y\to if\left(\left(x\in A\wedge 0\le v\right),v,0\right)=if\left(\left(y\in B\wedge 0\le v\right),v,0\right)$$
8	3 7	csbeq12dv	$$⊢x=y\to ⦋\Re \left(\frac{C}{{\mathrm{i}}^t}\right)/v⦌if\left(\left(x\in A\wedge 0\le v\right),v,0\right)=⦋\Re \left(\frac{D}{{\mathrm{i}}^t}\right)/v⦌if\left(\left(y\in B\wedge 0\le v\right),v,0\right)$$
9	8	cbvmptv	$$⊢\left(x\in ℝ⟼⦋\Re \left(\frac{C}{{\mathrm{i}}^t}\right)/v⦌if\left(\left(x\in A\wedge 0\le v\right),v,0\right)\right)=\left(y\in ℝ⟼⦋\Re \left(\frac{D}{{\mathrm{i}}^t}\right)/v⦌if\left(\left(y\in B\wedge 0\le v\right),v,0\right)\right)$$
10	9	fveq2i	$$⊢{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{C}{{\mathrm{i}}^t}\right)/v⦌if\left(\left(x\in A\wedge 0\le v\right),v,0\right)\right)\right)={\int }^2\left(\left(y\in ℝ⟼⦋\Re \left(\frac{D}{{\mathrm{i}}^t}\right)/v⦌if\left(\left(y\in B\wedge 0\le v\right),v,0\right)\right)\right)$$
11	10	oveq2i	$$⊢{\mathrm{i}}^t{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{C}{{\mathrm{i}}^t}\right)/v⦌if\left(\left(x\in A\wedge 0\le v\right),v,0\right)\right)\right)={\mathrm{i}}^t{\int }^2\left(\left(y\in ℝ⟼⦋\Re \left(\frac{D}{{\mathrm{i}}^t}\right)/v⦌if\left(\left(y\in B\wedge 0\le v\right),v,0\right)\right)\right)$$
12	11	sumeq2si	$$⊢\sum _{t=0}^3{\mathrm{i}}^t{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{C}{{\mathrm{i}}^t}\right)/v⦌if\left(\left(x\in A\wedge 0\le v\right),v,0\right)\right)\right)=\sum _{t=0}^3{\mathrm{i}}^t{\int }^2\left(\left(y\in ℝ⟼⦋\Re \left(\frac{D}{{\mathrm{i}}^t}\right)/v⦌if\left(\left(y\in B\wedge 0\le v\right),v,0\right)\right)\right)$$
13		df-itg	$$⊢{\int }_{A}Cdx=\sum _{t=0}^3{\mathrm{i}}^t{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{C}{{\mathrm{i}}^t}\right)/v⦌if\left(\left(x\in A\wedge 0\le v\right),v,0\right)\right)\right)$$
14		df-itg	$$⊢{\int }_{B}Ddy=\sum _{t=0}^3{\mathrm{i}}^t{\int }^2\left(\left(y\in ℝ⟼⦋\Re \left(\frac{D}{{\mathrm{i}}^t}\right)/v⦌if\left(\left(y\in B\wedge 0\le v\right),v,0\right)\right)\right)$$
15	12 13 14	3eqtr4i	$$⊢{\int }_{A}Cdx={\int }_{B}Ddy$$