Theorem dfitg

Description: Evaluate the class substitution in df-itg . (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Hypothesis	dfitg.1	$$⊢T=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
Assertion	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 T\right),T,0\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfitg.1	$$⊢T=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
2		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)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)\right)\right)$$
3		fvex	$$⊢\Re \left(\frac{B}{{\mathrm{i}}^k}\right)\in \mathrm{V}$$
4		id	$$⊢y=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)\to y=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
5	4 1	eqtr4di	$$⊢y=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)\to y=T$$
6	5	breq2d	$$⊢y=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)\to \left(0\le y\leftrightarrow 0\le T\right)$$
7	6	anbi2d	$$⊢y=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)\to \left(\left(x\in A\wedge 0\le y\right)\leftrightarrow \left(x\in A\wedge 0\le T\right)\right)$$
8	7 5	ifbieq1d	$$⊢y=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)\to if\left(\left(x\in A\wedge 0\le y\right),y,0\right)=if\left(\left(x\in A\wedge 0\le T\right),T,0\right)$$
9	3 8	csbie	$$⊢⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)=if\left(\left(x\in A\wedge 0\le T\right),T,0\right)$$
10	9	mpteq2i	$$⊢\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le T\right),T,0\right)\right)$$
11	10	fveq2i	$$⊢{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le T\right),T,0\right)\right)\right)$$
12	11	oveq2i	$$⊢{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)\right)\right)={\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le T\right),T,0\right)\right)\right)$$
13	12	a1i	$$⊢k\in \left(0\dots 3\right)\to {\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)\right)\right)={\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le T\right),T,0\right)\right)\right)$$
14	13	sumeq2i	$$⊢\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)\right)\right)=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le T\right),T,0\right)\right)\right)$$
15	2 14	eqtri	$$⊢{\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 T\right),T,0\right)\right)\right)$$