Theorem itgvallem3

Description: Lemma for itgposval and itgreval . (Contributed by Mario Carneiro, 7-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Hypothesis	itgvallem3.1	$$⊢\left(\phi \wedge x\in A\right)\to B=0$$
Assertion	itgvallem3	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le B\right),B,0\right)\right)\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		itgvallem3.1	$$⊢\left(\phi \wedge x\in A\right)\to B=0$$
2	1	adantrr	$$⊢\left(\phi \wedge \left(x\in A\wedge 0\le B\right)\right)\to B=0$$
3	2	ifeq1da	$$⊢\phi \to if\left(\left(x\in A\wedge 0\le B\right),B,0\right)=if\left(\left(x\in A\wedge 0\le B\right),0,0\right)$$
4		ifid	$$⊢if\left(\left(x\in A\wedge 0\le B\right),0,0\right)=0$$
5	3 4	eqtrdi	$$⊢\phi \to if\left(\left(x\in A\wedge 0\le B\right),B,0\right)=0$$
6	5	mpteq2dv	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le B\right),B,0\right)\right)=\left(x\in ℝ⟼0\right)$$
7		fconstmpt	$$⊢ℝ\times \left\{0\right\}=\left(x\in ℝ⟼0\right)$$
8	6 7	eqtr4di	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le B\right),B,0\right)\right)=ℝ\times \left\{0\right\}$$
9	8	fveq2d	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le B\right),B,0\right)\right)\right)={\int }^2\left(ℝ\times \left\{0\right\}\right)$$
10		itg20	$$⊢{\int }^2\left(ℝ\times \left\{0\right\}\right)=0$$
11	9 10	eqtrdi	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le B\right),B,0\right)\right)\right)=0$$