Theorem cbvitgv

Description: Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Hypothesis	cbvitg.1	$$⊢x=y\to B=C$$
Assertion	cbvitgv	$$⊢{\int }_{A}Bdx={\int }_{A}Cdy$$

Proof

Step	Hyp	Ref	Expression
1		cbvitg.1	$$⊢x=y\to B=C$$
2	1	fvoveq1d	$$⊢x=y\to \Re \left(\frac{B}{{\mathrm{i}}^k}\right)=\Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
3		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
4	3	anbi1d	$$⊢x=y\to \left(\left(x\in A\wedge 0\le v\right)\leftrightarrow \left(y\in A\wedge 0\le v\right)\right)$$
5	4	ifbid	$$⊢x=y\to if\left(\left(x\in A\wedge 0\le v\right),v,0\right)=if\left(\left(y\in A\wedge 0\le v\right),v,0\right)$$
6	2 5	csbeq12dv	$$⊢x=y\to ⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/v⦌if\left(\left(x\in A\wedge 0\le v\right),v,0\right)=⦋\Re \left(\frac{C}{{\mathrm{i}}^k}\right)/v⦌if\left(\left(y\in A\wedge 0\le v\right),v,0\right)$$
7	6	cbvmptv	$$⊢\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/v⦌if\left(\left(x\in A\wedge 0\le v\right),v,0\right)\right)=\left(y\in ℝ⟼⦋\Re \left(\frac{C}{{\mathrm{i}}^k}\right)/v⦌if\left(\left(y\in A\wedge 0\le v\right),v,0\right)\right)$$
8	7	fveq2i	$$⊢{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\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{C}{{\mathrm{i}}^k}\right)/v⦌if\left(\left(y\in A\wedge 0\le v\right),v,0\right)\right)\right)$$
9	8	oveq2i	$$⊢{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/v⦌if\left(\left(x\in A\wedge 0\le v\right),v,0\right)\right)\right)={\mathrm{i}}^k{\int }^2\left(\left(y\in ℝ⟼⦋\Re \left(\frac{C}{{\mathrm{i}}^k}\right)/v⦌if\left(\left(y\in A\wedge 0\le v\right),v,0\right)\right)\right)$$
10	9	a1i	$$⊢\top \to {\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/v⦌if\left(\left(x\in A\wedge 0\le v\right),v,0\right)\right)\right)={\mathrm{i}}^k{\int }^2\left(\left(y\in ℝ⟼⦋\Re \left(\frac{C}{{\mathrm{i}}^k}\right)/v⦌if\left(\left(y\in A\wedge 0\le v\right),v,0\right)\right)\right)$$
11	10	sumeq2sdv	$$⊢\top \to \sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/v⦌if\left(\left(x\in A\wedge 0\le v\right),v,0\right)\right)\right)=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(y\in ℝ⟼⦋\Re \left(\frac{C}{{\mathrm{i}}^k}\right)/v⦌if\left(\left(y\in A\wedge 0\le v\right),v,0\right)\right)\right)$$
12	11	mptru	$$⊢\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/v⦌if\left(\left(x\in A\wedge 0\le v\right),v,0\right)\right)\right)=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(y\in ℝ⟼⦋\Re \left(\frac{C}{{\mathrm{i}}^k}\right)/v⦌if\left(\left(y\in A\wedge 0\le v\right),v,0\right)\right)\right)$$
13		df-itg	$$⊢{\int }_{A}Bdx=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/v⦌if\left(\left(x\in A\wedge 0\le v\right),v,0\right)\right)\right)$$
14		df-itg	$$⊢{\int }_{A}Cdy=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(y\in ℝ⟼⦋\Re \left(\frac{C}{{\mathrm{i}}^k}\right)/v⦌if\left(\left(y\in A\wedge 0\le v\right),v,0\right)\right)\right)$$
15	12 13 14	3eqtr4i	$$⊢{\int }_{A}Bdx={\int }_{A}Cdy$$