Metamath Proof Explorer

Theorem mbfpos

Description: The positive part of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014)

Ref Expression
Hypotheses mbfpos.1 
|- ( ( ph /\ x e. A ) -> B e. RR )
mbfpos.2 
|- ( ph -> ( x e. A |-> B ) e. MblFn )
Assertion mbfpos 
|- ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfpos.1 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
2 mbfpos.2 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
3 c0ex 
 |-  0 e. _V
4 3 fvconst2 
 |-  ( x e. A -> ( ( A X. { 0 } ) ` x ) = 0 )
5 4 adantl 
 |-  ( ( ph /\ x e. A ) -> ( ( A X. { 0 } ) ` x ) = 0 )
6 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
7 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
8 7 fvmpt2 
 |-  ( ( x e. A /\ B e. RR ) -> ( ( x e. A |-> B ) ` x ) = B )
9 6 1 8 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
10 5 9 breq12d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( A X. { 0 } ) ` x ) <_ ( ( x e. A |-> B ) ` x ) <-> 0 <_ B ) )
11 10 9 5 ifbieq12d 
 |-  ( ( ph /\ x e. A ) -> if ( ( ( A X. { 0 } ) ` x ) <_ ( ( x e. A |-> B ) ` x ) , ( ( x e. A |-> B ) ` x ) , ( ( A X. { 0 } ) ` x ) ) = if ( 0 <_ B , B , 0 ) )
12 11 mpteq2dva 
 |-  ( ph -> ( x e. A |-> if ( ( ( A X. { 0 } ) ` x ) <_ ( ( x e. A |-> B ) ` x ) , ( ( x e. A |-> B ) ` x ) , ( ( A X. { 0 } ) ` x ) ) ) = ( x e. A |-> if ( 0 <_ B , B , 0 ) ) )
13 0re 
 |-  0 e. RR
14 13 fconst6 
 |-  ( A X. { 0 } ) : A --> RR
15 14 a1i 
 |-  ( ph -> ( A X. { 0 } ) : A --> RR )
16 2 1 mbfdm2 
 |-  ( ph -> A e. dom vol )
17 0cnd 
 |-  ( ph -> 0 e. CC )
18 mbfconst 
 |-  ( ( A e. dom vol /\ 0 e. CC ) -> ( A X. { 0 } ) e. MblFn )
19 16 17 18 syl2anc 
 |-  ( ph -> ( A X. { 0 } ) e. MblFn )
20 1 fmpttd 
 |-  ( ph -> ( x e. A |-> B ) : A --> RR )
21 nfcv 
 |-  F/_ y if ( ( ( A X. { 0 } ) ` x ) <_ ( ( x e. A |-> B ) ` x ) , ( ( x e. A |-> B ) ` x ) , ( ( A X. { 0 } ) ` x ) )
22 nfcv 
 |-  F/_ x ( ( A X. { 0 } ) ` y )
23 nfcv 
 |-  F/_ x <_
24 nffvmpt1 
 |-  F/_ x ( ( x e. A |-> B ) ` y )
25 22 23 24 nfbr 
 |-  F/ x ( ( A X. { 0 } ) ` y ) <_ ( ( x e. A |-> B ) ` y )
26 25 24 22 nfif 
 |-  F/_ x if ( ( ( A X. { 0 } ) ` y ) <_ ( ( x e. A |-> B ) ` y ) , ( ( x e. A |-> B ) ` y ) , ( ( A X. { 0 } ) ` y ) )
27 fveq2 
 |-  ( x = y -> ( ( A X. { 0 } ) ` x ) = ( ( A X. { 0 } ) ` y ) )
28 fveq2 
 |-  ( x = y -> ( ( x e. A |-> B ) ` x ) = ( ( x e. A |-> B ) ` y ) )
29 27 28 breq12d 
 |-  ( x = y -> ( ( ( A X. { 0 } ) ` x ) <_ ( ( x e. A |-> B ) ` x ) <-> ( ( A X. { 0 } ) ` y ) <_ ( ( x e. A |-> B ) ` y ) ) )
30 29 28 27 ifbieq12d 
 |-  ( x = y -> if ( ( ( A X. { 0 } ) ` x ) <_ ( ( x e. A |-> B ) ` x ) , ( ( x e. A |-> B ) ` x ) , ( ( A X. { 0 } ) ` x ) ) = if ( ( ( A X. { 0 } ) ` y ) <_ ( ( x e. A |-> B ) ` y ) , ( ( x e. A |-> B ) ` y ) , ( ( A X. { 0 } ) ` y ) ) )
31 21 26 30 cbvmpt 
 |-  ( x e. A |-> if ( ( ( A X. { 0 } ) ` x ) <_ ( ( x e. A |-> B ) ` x ) , ( ( x e. A |-> B ) ` x ) , ( ( A X. { 0 } ) ` x ) ) ) = ( y e. A |-> if ( ( ( A X. { 0 } ) ` y ) <_ ( ( x e. A |-> B ) ` y ) , ( ( x e. A |-> B ) ` y ) , ( ( A X. { 0 } ) ` y ) ) )
32 15 19 20 2 31 mbfmax 
 |-  ( ph -> ( x e. A |-> if ( ( ( A X. { 0 } ) ` x ) <_ ( ( x e. A |-> B ) ` x ) , ( ( x e. A |-> B ) ` x ) , ( ( A X. { 0 } ) ` x ) ) ) e. MblFn )
33 12 32 eqeltrrd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )