# 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 ( ( 𝜑𝑥𝐴 ) → 𝐵 = 0 )
Assertion itgvallem3 ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) = 0 )

### Proof

Step Hyp Ref Expression
1 itgvallem3.1 ( ( 𝜑𝑥𝐴 ) → 𝐵 = 0 )
2 1 adantrr ( ( 𝜑 ∧ ( 𝑥𝐴 ∧ 0 ≤ 𝐵 ) ) → 𝐵 = 0 )
3 2 ifeq1da ( 𝜑 → if ( ( 𝑥𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) = if ( ( 𝑥𝐴 ∧ 0 ≤ 𝐵 ) , 0 , 0 ) )
4 ifid if ( ( 𝑥𝐴 ∧ 0 ≤ 𝐵 ) , 0 , 0 ) = 0
5 3 4 eqtrdi ( 𝜑 → if ( ( 𝑥𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) = 0 )
6 5 mpteq2dv ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ 0 ) )
7 fconstmpt ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 )
8 6 7 eqtr4di ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) = ( ℝ × { 0 } ) )
9 8 fveq2d ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) = ( ∫2 ‘ ( ℝ × { 0 } ) ) )
10 itg20 ( ∫2 ‘ ( ℝ × { 0 } ) ) = 0
11 9 10 eqtrdi ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) = 0 )