Theorem itgresr

Description: The domain of an integral only matters in its intersection with RR . (Contributed by Mario Carneiro, 29-Jun-2014)

	Ref	Expression
Assertion	itgresr	$$⊢{\int }_{A}Bdx={\int }_{\left(A\cap ℝ\right)}Bdx$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(k\in \left(0\dots 3\right)\wedge x\in ℝ\right)\to x\in ℝ$$
2	1	biantrud	$$⊢\left(k\in \left(0\dots 3\right)\wedge x\in ℝ\right)\to \left(x\in A\leftrightarrow \left(x\in A\wedge x\in ℝ\right)\right)$$
3		elin	$$⊢x\in \left(A\cap ℝ\right)\leftrightarrow \left(x\in A\wedge x\in ℝ\right)$$
4	2 3	bitr4di	$$⊢\left(k\in \left(0\dots 3\right)\wedge x\in ℝ\right)\to \left(x\in A\leftrightarrow x\in \left(A\cap ℝ\right)\right)$$
5	4	anbi1d	$$⊢\left(k\in \left(0\dots 3\right)\wedge x\in ℝ\right)\to \left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right)\leftrightarrow \left(x\in \left(A\cap ℝ\right)\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right)\right)$$
6	5	ifbid	$$⊢\left(k\in \left(0\dots 3\right)\wedge x\in ℝ\right)\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(x\in \left(A\cap ℝ\right)\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)$$
7	6	mpteq2dva	$$⊢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(x\in ℝ⟼if\left(\left(x\in \left(A\cap ℝ\right)\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)$$
8	7	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(x\in ℝ⟼if\left(\left(x\in \left(A\cap ℝ\right)\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
9	8	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(x\in ℝ⟼if\left(\left(x\in \left(A\cap ℝ\right)\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
10	9	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(x\in ℝ⟼if\left(\left(x\in \left(A\cap ℝ\right)\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
11		eqid	$$⊢\Re \left(\frac{B}{{\mathrm{i}}^k}\right)=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
12	11	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)$$
13	11	dfitg	$$⊢{\int }_{\left(A\cap ℝ\right)}Bdx=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \left(A\cap ℝ\right)\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
14	10 12 13	3eqtr4i	$$⊢{\int }_{A}Bdx={\int }_{\left(A\cap ℝ\right)}Bdx$$