Metamath Proof Explorer

Theorem itgposval

Description: The integral of a nonnegative function. (Contributed by Mario Carneiro, 31-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses iblrelem.1 ⊢ φ ∧ x ∈ A → B ∈ ℝ
itgreval.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
itgposval.3 ⊢ φ ∧ x ∈ A → 0 ≤ B
Assertion itgposval ⊢ φ → ∫ A B dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0

Proof

Step Hyp Ref Expression
1 iblrelem.1 ⊢ φ ∧ x ∈ A → B ∈ ℝ
2 itgreval.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
3 itgposval.3 ⊢ φ ∧ x ∈ A → 0 ≤ B
4 1 2 itgrevallem1 ⊢ φ → ∫ A B dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0
5 3 ex ⊢ φ → x ∈ A → 0 ≤ B
6 5 pm4.71rd ⊢ φ → x ∈ A ↔ 0 ≤ B ∧ x ∈ A
7 ancom ⊢ 0 ≤ B ∧ x ∈ A ↔ x ∈ A ∧ 0 ≤ B
8 6 7 bitr2di ⊢ φ → x ∈ A ∧ 0 ≤ B ↔ x ∈ A
9 8 ifbid ⊢ φ → if x ∈ A ∧ 0 ≤ B B 0 = if x ∈ A B 0
10 9 mpteq2dv ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 = x ∈ ℝ ⟼ if x ∈ A B 0
11 10 fveq2d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0
12 1 3 iblposlem ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 = 0
13 11 12 oveq12d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 − 0
14 1 3 iblpos ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
15 2 14 mpbid ⊢ φ → x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
16 15 simprd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
17 16 recnd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℂ
18 17 subid1d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 − 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0
19 4 13 18 3eqtrd ⊢ φ → ∫ A B dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0