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 ⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
Assertion i1fpos ( 𝐹 ∈ dom ∫1 → 𝐺 ∈ dom ∫1 )

Proof

Step Hyp Ref Expression
1 i1fpos.1 ⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
2 simpr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
3 2 biantrurd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) ) )
4 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
5 4 ffvelcdmda ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
6 5 biantrurd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ) )
7 elrege0 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
8 6 7 bitr4di ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) )
9 4 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℝ )
10 ffn ⊢ ( 𝐹 : ℝ ⟶ ℝ → 𝐹 Fn ℝ )
11 elpreima ⊢ ( 𝐹 Fn ℝ → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) ) )
12 9 10 11 3syl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) ) )
13 3 8 12 3bitr4d ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) ) )
14 13 ifbid ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
15 14 mpteq2dva ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
16 1 15 eqtrid ⊢ ( 𝐹 ∈ dom ∫1 → 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
17 i1fima ⊢ ( 𝐹 ∈ dom ∫1 → ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) ∈ dom vol )
18 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
19 18 i1fres ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) ∈ dom vol ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 )
20 17 19 mpdan ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 )
21 16 20 eqeltrd ⊢ ( 𝐹 ∈ dom ∫1 → 𝐺 ∈ dom ∫1 )