Theorem itgeq2

Description: Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Assertion	itgeq2	$$⊢\forall x\in AB=C\to {\int }_{A}Bdx={\int }_{A}Cdx$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢ℝ=ℝ$$
2		simpl	$$⊢\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right)\to x\in A$$
3	2	con3i	$$⊢\neg x\in A\to \neg \left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right)$$
4	3	iffalsed	$$⊢\neg x\in A\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)=0$$
5		simpl	$$⊢\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)\to x\in A$$
6	5	con3i	$$⊢\neg x\in A\to \neg \left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)$$
7	6	iffalsed	$$⊢\neg x\in A\to if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)=0$$
8	4 7	eqtr4d	$$⊢\neg x\in A\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 A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
9		fvoveq1	$$⊢B=C\to \Re \left(\frac{B}{{\mathrm{i}}^k}\right)=\Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
10	9	breq2d	$$⊢B=C\to \left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\leftrightarrow 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)$$
11	10	anbi2d	$$⊢B=C\to \left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right)\leftrightarrow \left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)\right)$$
12	11 9	ifbieq1d	$$⊢B=C\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 A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
13	8 12	ja	$$⊢\left(x\in A\to B=C\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 A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
14	13	a1d	$$⊢\left(x\in A\to B=C\right)\to \left(x\in ℝ\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 A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
15	14	ralimi2	$$⊢\forall x\in AB=C\to \forall 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)=if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
16		mpteq12	$$⊢\left(ℝ=ℝ\wedge \forall 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)=if\left(\left(x\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)\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 A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
17	1 15 16	sylancr	$$⊢\forall x\in AB=C\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 A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
18	17	fveq2d	$$⊢\forall x\in AB=C\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 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)$$
19	18	oveq2d	$$⊢\forall x\in AB=C\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 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)$$
20	19	sumeq2sdv	$$⊢\forall x\in AB=C\to \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 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)$$
21		eqid	$$⊢\Re \left(\frac{B}{{\mathrm{i}}^k}\right)=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
22	21	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)$$
23		eqid	$$⊢\Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
24	23	dfitg	$$⊢{\int }_{A}Cdx=\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{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
25	20 22 24	3eqtr4g	$$⊢\forall x\in AB=C\to {\int }_{A}Bdx={\int }_{A}Cdx$$