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 ffvelrnda ( ( 𝐹 ∈ 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 syl5eq ( 𝐹 ∈ 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 )