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 e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) )
Assertion i1fpos 
|- ( F e. dom S.1 -> G e. dom S.1 )

Proof

Step Hyp Ref Expression
1 i1fpos.1 
 |-  G = ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) )
2 simpr 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> x e. RR )
3 2 biantrurd 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( x e. RR /\ ( F ` x ) e. ( 0 [,) +oo ) ) ) )
4 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
5 4 ffvelrnda 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> ( F ` x ) e. RR )
6 5 biantrurd 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> ( 0 <_ ( F ` x ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) ) )
7 elrege0 
 |-  ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
8 6 7 bitr4di 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> ( 0 <_ ( F ` x ) <-> ( F ` x ) e. ( 0 [,) +oo ) ) )
9 4 adantr 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> F : RR --> RR )
10 ffn 
 |-  ( F : RR --> RR -> F Fn RR )
11 elpreima 
 |-  ( F Fn RR -> ( x e. ( `' F " ( 0 [,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( 0 [,) +oo ) ) ) )
12 9 10 11 3syl 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> ( x e. ( `' F " ( 0 [,) +oo ) ) <-> ( x e. RR /\ ( F ` x ) e. ( 0 [,) +oo ) ) ) )
13 3 8 12 3bitr4d 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> ( 0 <_ ( F ` x ) <-> x e. ( `' F " ( 0 [,) +oo ) ) ) )
14 13 ifbid 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) = if ( x e. ( `' F " ( 0 [,) +oo ) ) , ( F ` x ) , 0 ) )
15 14 mpteq2dva 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. ( `' F " ( 0 [,) +oo ) ) , ( F ` x ) , 0 ) ) )
16 1 15 eqtrid 
 |-  ( F e. dom S.1 -> G = ( x e. RR |-> if ( x e. ( `' F " ( 0 [,) +oo ) ) , ( F ` x ) , 0 ) ) )
17 i1fima 
 |-  ( F e. dom S.1 -> ( `' F " ( 0 [,) +oo ) ) e. dom vol )
18 eqid 
 |-  ( x e. RR |-> if ( x e. ( `' F " ( 0 [,) +oo ) ) , ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. ( `' F " ( 0 [,) +oo ) ) , ( F ` x ) , 0 ) )
19 18 i1fres 
 |-  ( ( F e. dom S.1 /\ ( `' F " ( 0 [,) +oo ) ) e. dom vol ) -> ( x e. RR |-> if ( x e. ( `' F " ( 0 [,) +oo ) ) , ( F ` x ) , 0 ) ) e. dom S.1 )
20 17 19 mpdan 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( x e. ( `' F " ( 0 [,) +oo ) ) , ( F ` x ) , 0 ) ) e. dom S.1 )
21 16 20 eqeltrd 
 |-  ( F e. dom S.1 -> G e. dom S.1 )