Theorem itgeq12dv

Description: Equality theorem for an integral. (Contributed by Thierry Arnoux, 14-Feb-2017)

	Ref	Expression
Hypotheses	itgeq12dv.2	$$⊢\phi \to A=B$$
	itgeq12dv.1	$$⊢\left(\phi \wedge x\in A\right)\to C=D$$
Assertion	itgeq12dv	$$⊢\phi \to {\int }_{A}Cdx={\int }_{B}Ddx$$

Proof

Step	Hyp	Ref	Expression
1		itgeq12dv.2	$$⊢\phi \to A=B$$
2		itgeq12dv.1	$$⊢\left(\phi \wedge x\in A\right)\to C=D$$
3	2	fvoveq1d	$$⊢\left(\phi \wedge x\in A\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(\frac{D}{{\mathrm{i}}^k}\right)$$
4	3	breq2d	$$⊢\left(\phi \wedge x\in A\right)\to \left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\leftrightarrow 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right)$$
5	4	pm5.32da	$$⊢\phi \to \left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)\leftrightarrow \left(x\in A\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right)\right)$$
6	1	eleq2d	$$⊢\phi \to \left(x\in A\leftrightarrow x\in B\right)$$
7	6	anbi1d	$$⊢\phi \to \left(\left(x\in A\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right)\leftrightarrow \left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right)\right)$$
8	5 7	bitrd	$$⊢\phi \to \left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)\leftrightarrow \left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right)\right)$$
9	3	adantrr	$$⊢\left(\phi \wedge \left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(\frac{D}{{\mathrm{i}}^k}\right)$$
10		eqidd	$$⊢\left(\phi \wedge \neg \left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)\right)\to 0=0$$
11	8 9 10	ifbieq12d2	$$⊢\phi \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)=if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)$$
12	11	mpteq2dv	$$⊢\phi \to \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)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)$$
13	12	fveq2d	$$⊢\phi \to {\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)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
14	13	oveq2d	$$⊢\phi \to {\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)={\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
15	14	sumeq2sdv	$$⊢\phi \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{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\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 B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
16		eqid	$$⊢\Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
17	16	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)$$
18		eqid	$$⊢\Re \left(\frac{D}{{\mathrm{i}}^k}\right)=\Re \left(\frac{D}{{\mathrm{i}}^k}\right)$$
19	18	dfitg	$$⊢{\int }_{B}Ddx=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
20	15 17 19	3eqtr4g	$$⊢\phi \to {\int }_{A}Cdx={\int }_{B}Ddx$$