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 ∈ ℝ ⟼ if 0 ≤ F ⁡ x F ⁡ x 0
Assertion i1fpos ⊢ F ∈ dom ⁡ ∫ 1 → G ∈ dom ⁡ ∫ 1

Proof

Step Hyp Ref Expression
1 i1fpos.1 ⊢ G = x ∈ ℝ ⟼ if 0 ≤ F ⁡ x F ⁡ x 0
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 ffvelrnda ⊢ 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 : ℝ ⟶ ℝ → F Fn ℝ
11 elpreima ⊢ F Fn ℝ → x ∈ F -1 0 +∞ ↔ x ∈ ℝ ∧ F ⁡ x ∈ 0 +∞
12 9 10 11 3syl ⊢ F ∈ dom ⁡ ∫ 1 ∧ x ∈ ℝ → x ∈ F -1 0 +∞ ↔ x ∈ ℝ ∧ F ⁡ x ∈ 0 +∞
13 3 8 12 3bitr4d ⊢ F ∈ dom ⁡ ∫ 1 ∧ x ∈ ℝ → 0 ≤ F ⁡ x ↔ x ∈ F -1 0 +∞
14 13 ifbid ⊢ F ∈ dom ⁡ ∫ 1 ∧ x ∈ ℝ → if 0 ≤ F ⁡ x F ⁡ x 0 = if x ∈ F -1 0 +∞ F ⁡ x 0
15 14 mpteq2dva ⊢ F ∈ dom ⁡ ∫ 1 → x ∈ ℝ ⟼ if 0 ≤ F ⁡ x F ⁡ x 0 = x ∈ ℝ ⟼ if x ∈ F -1 0 +∞ F ⁡ x 0
16 1 15 syl5eq ⊢ F ∈ dom ⁡ ∫ 1 → G = x ∈ ℝ ⟼ if x ∈ F -1 0 +∞ F ⁡ x 0
17 i1fima ⊢ F ∈ dom ⁡ ∫ 1 → F -1 0 +∞ ∈ dom ⁡ vol
18 eqid ⊢ x ∈ ℝ ⟼ if x ∈ F -1 0 +∞ F ⁡ x 0 = x ∈ ℝ ⟼ if x ∈ F -1 0 +∞ F ⁡ x 0
19 18 i1fres ⊢ F ∈ dom ⁡ ∫ 1 ∧ F -1 0 +∞ ∈ dom ⁡ vol → x ∈ ℝ ⟼ if x ∈ F -1 0 +∞ F ⁡ x 0 ∈ dom ⁡ ∫ 1
20 17 19 mpdan ⊢ F ∈ dom ⁡ ∫ 1 → x ∈ ℝ ⟼ if x ∈ F -1 0 +∞ F ⁡ x 0 ∈ dom ⁡ ∫ 1
21 16 20 eqeltrd ⊢ F ∈ dom ⁡ ∫ 1 → G ∈ dom ⁡ ∫ 1