Metamath Proof Explorer

Theorem i1fpos

Description: The positive part of a simple function is simple. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Hypothesis i1fpos.1 ⊢G=x∈ℝ⟼if0≤F⁡xF⁡x0
Assertion i1fpos ⊢F∈dom⁡∫1→G∈dom⁡∫1

Proof

Step Hyp Ref Expression
1 i1fpos.1 ⊢G=x∈ℝ⟼if0≤F⁡xF⁡x0
2 simpr ⊢F∈dom⁡∫1∧x∈ℝ→x∈ℝ
3 2 biantrurd ⊢F∈dom⁡∫1∧x∈ℝ→F⁡x∈0+∞↔x∈ℝ∧F⁡x∈0+∞
4 i1ff ⊢F∈dom⁡∫1→F:ℝ⟶ℝ
5 4 ffvelcdmda ⊢F∈dom⁡∫1∧x∈ℝ→F⁡x∈ℝ
6 5 biantrurd ⊢F∈dom⁡∫1∧x∈ℝ→0≤F⁡x↔F⁡x∈ℝ∧0≤F⁡x
7 elrege0 ⊢F⁡x∈0+∞↔F⁡x∈ℝ∧0≤F⁡x
8 6 7 bitr4di ⊢F∈dom⁡∫1∧x∈ℝ→0≤F⁡x↔F⁡x∈0+∞
9 4 adantr ⊢F∈dom⁡∫1∧x∈ℝ→F:ℝ⟶ℝ
10 ffn ⊢F:ℝ⟶ℝ→FFnℝ
11 elpreima ⊢FFnℝ→x∈F-10+∞↔x∈ℝ∧F⁡x∈0+∞
12 9 10 11 3syl ⊢F∈dom⁡∫1∧x∈ℝ→x∈F-10+∞↔x∈ℝ∧F⁡x∈0+∞
13 3 8 12 3bitr4d ⊢F∈dom⁡∫1∧x∈ℝ→0≤F⁡x↔x∈F-10+∞
14 13 ifbid ⊢F∈dom⁡∫1∧x∈ℝ→if0≤F⁡xF⁡x0=ifx∈F-10+∞F⁡x0
15 14 mpteq2dva ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤F⁡xF⁡x0=x∈ℝ⟼ifx∈F-10+∞F⁡x0
16 1 15 eqtrid ⊢F∈dom⁡∫1→G=x∈ℝ⟼ifx∈F-10+∞F⁡x0
17 i1fima ⊢F∈dom⁡∫1→F-10+∞∈dom⁡vol
18 eqid ⊢x∈ℝ⟼ifx∈F-10+∞F⁡x0=x∈ℝ⟼ifx∈F-10+∞F⁡x0
19 18 i1fres ⊢F∈dom⁡∫1∧F-10+∞∈dom⁡vol→x∈ℝ⟼ifx∈F-10+∞F⁡x0∈dom⁡∫1
20 17 19 mpdan ⊢F∈dom⁡∫1→x∈ℝ⟼ifx∈F-10+∞F⁡x0∈dom⁡∫1
21 16 20 eqeltrd ⊢F∈dom⁡∫1→G∈dom⁡∫1