# Metamath Proof Explorer

## 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 syl6eq ${⊢}{\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 ${⊢}ℝ×\left\{0\right\}=\left({x}\in ℝ⟼0\right)$
8 6 7 syl6eqr ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)=ℝ×\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(ℝ×\left\{0\right\}\right)$
10 itg20 ${⊢}{\int }^{2}\left(ℝ×\left\{0\right\}\right)=0$
11 9 10 syl6eq ${⊢}{\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$