Theorem cbvitg

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

	Ref	Expression
Hypotheses	cbvitg.1	$$⊢x=y\to B=C$$
	cbvitg.2	$$⊢\underset{\_}{Ⅎ}yB$$
	cbvitg.3	$$⊢\underset{\_}{Ⅎ}xC$$
Assertion	cbvitg	$$⊢{\int }_{A}Bdx={\int }_{A}Cdy$$

Proof

Step	Hyp	Ref	Expression
1		cbvitg.1	$$⊢x=y\to B=C$$
2		cbvitg.2	$$⊢\underset{\_}{Ⅎ}yB$$
3		cbvitg.3	$$⊢\underset{\_}{Ⅎ}xC$$
4		nfv	$$⊢Ⅎyx\in A$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}y0$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}y\le$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}y\Re$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}y÷$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}y{\mathrm{i}}^k$$
10	2 8 9	nfov	$$⊢\underset{\_}{Ⅎ}y\left(\frac{B}{{\mathrm{i}}^k}\right)$$
11	7 10	nffv	$$⊢\underset{\_}{Ⅎ}y\Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
12	5 6 11	nfbr	$$⊢Ⅎy0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
13	4 12	nfan	$$⊢Ⅎy\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right)$$
14	13 11 5	nfif	$$⊢\underset{\_}{Ⅎ}yif\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)$$
15		nfv	$$⊢Ⅎxy\in A$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}x0$$
17		nfcv	$$⊢\underset{\_}{Ⅎ}x\le$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}x\Re$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}x÷$$
20		nfcv	$$⊢\underset{\_}{Ⅎ}x{\mathrm{i}}^k$$
21	3 19 20	nfov	$$⊢\underset{\_}{Ⅎ}x\left(\frac{C}{{\mathrm{i}}^k}\right)$$
22	18 21	nffv	$$⊢\underset{\_}{Ⅎ}x\Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
23	16 17 22	nfbr	$$⊢Ⅎx0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
24	15 23	nfan	$$⊢Ⅎx\left(y\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)$$
25	24 22 16	nfif	$$⊢\underset{\_}{Ⅎ}xif\left(\left(y\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
26		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
27	1	fvoveq1d	$$⊢x=y\to \Re \left(\frac{B}{{\mathrm{i}}^k}\right)=\Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
28	27	breq2d	$$⊢x=y\to \left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\leftrightarrow 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)$$
29	26 28	anbi12d	$$⊢x=y\to \left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right)\leftrightarrow \left(y\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)\right)$$
30	29 27	ifbieq1d	$$⊢x=y\to if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)=if\left(\left(y\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
31	14 25 30	cbvmpt	$$⊢\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)=\left(y\in ℝ⟼if\left(\left(y\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
32	31	a1i	$$⊢k\in \left(0\dots 3\right)\to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)=\left(y\in ℝ⟼if\left(\left(y\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
33	32	fveq2d	$$⊢k\in \left(0\dots 3\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)={\int }^2\left(\left(y\in ℝ⟼if\left(\left(y\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
34	33	oveq2d	$$⊢k\in \left(0\dots 3\right)\to {\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)={\mathrm{i}}^k{\int }^2\left(\left(y\in ℝ⟼if\left(\left(y\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
35	34	sumeq2i	$$⊢\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(y\in ℝ⟼if\left(\left(y\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
36		eqid	$$⊢\Re \left(\frac{B}{{\mathrm{i}}^k}\right)=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
37	36	dfitg	$$⊢{\int }_{A}Bdx=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
38		eqid	$$⊢\Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
39	38	dfitg	$$⊢{\int }_{A}Cdy=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(y\in ℝ⟼if\left(\left(y\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
40	35 37 39	3eqtr4i	$$⊢{\int }_{A}Bdx={\int }_{A}Cdy$$