Metamath Proof Explorer

Theorem mbfposb

Description: A function is measurable iff its positive and negative parts are measurable. (Contributed by Mario Carneiro, 11-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 mbfpos.1 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
2 nfcv 
 |-  F/_ x 0
3 nfcv 
 |-  F/_ x <_
4 nffvmpt1 
 |-  F/_ x ( ( x e. A |-> B ) ` y )
5 2 3 4 nfbr 
 |-  F/ x 0 <_ ( ( x e. A |-> B ) ` y )
6 5 4 2 nfif 
 |-  F/_ x if ( 0 <_ ( ( x e. A |-> B ) ` y ) , ( ( x e. A |-> B ) ` y ) , 0 )
7 nfcv 
 |-  F/_ y if ( 0 <_ ( ( x e. A |-> B ) ` x ) , ( ( x e. A |-> B ) ` x ) , 0 )
8 fveq2 
 |-  ( y = x -> ( ( x e. A |-> B ) ` y ) = ( ( x e. A |-> B ) ` x ) )
9 8 breq2d 
 |-  ( y = x -> ( 0 <_ ( ( x e. A |-> B ) ` y ) <-> 0 <_ ( ( x e. A |-> B ) ` x ) ) )
10 9 8 ifbieq1d 
 |-  ( y = x -> if ( 0 <_ ( ( x e. A |-> B ) ` y ) , ( ( x e. A |-> B ) ` y ) , 0 ) = if ( 0 <_ ( ( x e. A |-> B ) ` x ) , ( ( x e. A |-> B ) ` x ) , 0 ) )
11 6 7 10 cbvmpt 
 |-  ( y e. A |-> if ( 0 <_ ( ( x e. A |-> B ) ` y ) , ( ( x e. A |-> B ) ` y ) , 0 ) ) = ( x e. A |-> if ( 0 <_ ( ( x e. A |-> B ) ` x ) , ( ( x e. A |-> B ) ` x ) , 0 ) )
12 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
13 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
14 13 fvmpt2 
 |-  ( ( x e. A /\ B e. RR ) -> ( ( x e. A |-> B ) ` x ) = B )
15 12 1 14 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
16 15 breq2d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ ( ( x e. A |-> B ) ` x ) <-> 0 <_ B ) )
17 16 15 ifbieq1d 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( ( x e. A |-> B ) ` x ) , ( ( x e. A |-> B ) ` x ) , 0 ) = if ( 0 <_ B , B , 0 ) )
18 17 mpteq2dva 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ ( ( x e. A |-> B ) ` x ) , ( ( x e. A |-> B ) ` x ) , 0 ) ) = ( x e. A |-> if ( 0 <_ B , B , 0 ) ) )
19 11 18 syl5eq 
 |-  ( ph -> ( y e. A |-> if ( 0 <_ ( ( x e. A |-> B ) ` y ) , ( ( x e. A |-> B ) ` y ) , 0 ) ) = ( x e. A |-> if ( 0 <_ B , B , 0 ) ) )
20 19 adantr 
 |-  ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( y e. A |-> if ( 0 <_ ( ( x e. A |-> B ) ` y ) , ( ( x e. A |-> B ) ` y ) , 0 ) ) = ( x e. A |-> if ( 0 <_ B , B , 0 ) ) )
21 1 fmpttd 
 |-  ( ph -> ( x e. A |-> B ) : A --> RR )
22 21 adantr 
 |-  ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( x e. A |-> B ) : A --> RR )
23 22 ffvelrnda 
 |-  ( ( ( ph /\ ( x e. A |-> B ) e. MblFn ) /\ y e. A ) -> ( ( x e. A |-> B ) ` y ) e. RR )
24 nfcv 
 |-  F/_ y ( ( x e. A |-> B ) ` x )
25 4 24 8 cbvmpt 
 |-  ( y e. A |-> ( ( x e. A |-> B ) ` y ) ) = ( x e. A |-> ( ( x e. A |-> B ) ` x ) )
26 15 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( ( x e. A |-> B ) ` x ) ) = ( x e. A |-> B ) )
27 25 26 syl5eq 
 |-  ( ph -> ( y e. A |-> ( ( x e. A |-> B ) ` y ) ) = ( x e. A |-> B ) )
28 27 eleq1d 
 |-  ( ph -> ( ( y e. A |-> ( ( x e. A |-> B ) ` y ) ) e. MblFn <-> ( x e. A |-> B ) e. MblFn ) )
29 28 biimpar 
 |-  ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( y e. A |-> ( ( x e. A |-> B ) ` y ) ) e. MblFn )
30 23 29 mbfpos 
 |-  ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( y e. A |-> if ( 0 <_ ( ( x e. A |-> B ) ` y ) , ( ( x e. A |-> B ) ` y ) , 0 ) ) e. MblFn )
31 20 30 eqeltrrd 
 |-  ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
32 4 nfneg 
 |-  F/_ x -u ( ( x e. A |-> B ) ` y )
33 2 3 32 nfbr 
 |-  F/ x 0 <_ -u ( ( x e. A |-> B ) ` y )
34 33 32 2 nfif 
 |-  F/_ x if ( 0 <_ -u ( ( x e. A |-> B ) ` y ) , -u ( ( x e. A |-> B ) ` y ) , 0 )
35 nfcv 
 |-  F/_ y if ( 0 <_ -u ( ( x e. A |-> B ) ` x ) , -u ( ( x e. A |-> B ) ` x ) , 0 )
36 8 negeqd 
 |-  ( y = x -> -u ( ( x e. A |-> B ) ` y ) = -u ( ( x e. A |-> B ) ` x ) )
37 36 breq2d 
 |-  ( y = x -> ( 0 <_ -u ( ( x e. A |-> B ) ` y ) <-> 0 <_ -u ( ( x e. A |-> B ) ` x ) ) )
38 37 36 ifbieq1d 
 |-  ( y = x -> if ( 0 <_ -u ( ( x e. A |-> B ) ` y ) , -u ( ( x e. A |-> B ) ` y ) , 0 ) = if ( 0 <_ -u ( ( x e. A |-> B ) ` x ) , -u ( ( x e. A |-> B ) ` x ) , 0 ) )
39 34 35 38 cbvmpt 
 |-  ( y e. A |-> if ( 0 <_ -u ( ( x e. A |-> B ) ` y ) , -u ( ( x e. A |-> B ) ` y ) , 0 ) ) = ( x e. A |-> if ( 0 <_ -u ( ( x e. A |-> B ) ` x ) , -u ( ( x e. A |-> B ) ` x ) , 0 ) )
40 15 negeqd 
 |-  ( ( ph /\ x e. A ) -> -u ( ( x e. A |-> B ) ` x ) = -u B )
41 40 breq2d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ -u ( ( x e. A |-> B ) ` x ) <-> 0 <_ -u B ) )
42 41 40 ifbieq1d 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u ( ( x e. A |-> B ) ` x ) , -u ( ( x e. A |-> B ) ` x ) , 0 ) = if ( 0 <_ -u B , -u B , 0 ) )
43 42 mpteq2dva 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u ( ( x e. A |-> B ) ` x ) , -u ( ( x e. A |-> B ) ` x ) , 0 ) ) = ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) )
44 39 43 syl5eq 
 |-  ( ph -> ( y e. A |-> if ( 0 <_ -u ( ( x e. A |-> B ) ` y ) , -u ( ( x e. A |-> B ) ` y ) , 0 ) ) = ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) )
45 44 adantr 
 |-  ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( y e. A |-> if ( 0 <_ -u ( ( x e. A |-> B ) ` y ) , -u ( ( x e. A |-> B ) ` y ) , 0 ) ) = ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) )
46 23 renegcld 
 |-  ( ( ( ph /\ ( x e. A |-> B ) e. MblFn ) /\ y e. A ) -> -u ( ( x e. A |-> B ) ` y ) e. RR )
47 23 29 mbfneg 
 |-  ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( y e. A |-> -u ( ( x e. A |-> B ) ` y ) ) e. MblFn )
48 46 47 mbfpos 
 |-  ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( y e. A |-> if ( 0 <_ -u ( ( x e. A |-> B ) ` y ) , -u ( ( x e. A |-> B ) ` y ) , 0 ) ) e. MblFn )
49 45 48 eqeltrrd 
 |-  ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn )
50 31 49 jca 
 |-  ( ( ph /\ ( x e. A |-> B ) e. MblFn ) -> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn ) )
51 27 adantr 
 |-  ( ( ph /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn ) ) -> ( y e. A |-> ( ( x e. A |-> B ) ` y ) ) = ( x e. A |-> B ) )
52 21 ffvelrnda 
 |-  ( ( ph /\ y e. A ) -> ( ( x e. A |-> B ) ` y ) e. RR )
53 52 adantlr 
 |-  ( ( ( ph /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn ) ) /\ y e. A ) -> ( ( x e. A |-> B ) ` y ) e. RR )
54 19 adantr 
 |-  ( ( ph /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn ) ) -> ( y e. A |-> if ( 0 <_ ( ( x e. A |-> B ) ` y ) , ( ( x e. A |-> B ) ` y ) , 0 ) ) = ( x e. A |-> if ( 0 <_ B , B , 0 ) ) )
55 simprl 
 |-  ( ( ph /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn ) ) -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
56 54 55 eqeltrd 
 |-  ( ( ph /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn ) ) -> ( y e. A |-> if ( 0 <_ ( ( x e. A |-> B ) ` y ) , ( ( x e. A |-> B ) ` y ) , 0 ) ) e. MblFn )
57 44 adantr 
 |-  ( ( ph /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn ) ) -> ( y e. A |-> if ( 0 <_ -u ( ( x e. A |-> B ) ` y ) , -u ( ( x e. A |-> B ) ` y ) , 0 ) ) = ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) )
58 simprr 
 |-  ( ( ph /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn ) ) -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn )
59 57 58 eqeltrd 
 |-  ( ( ph /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn ) ) -> ( y e. A |-> if ( 0 <_ -u ( ( x e. A |-> B ) ` y ) , -u ( ( x e. A |-> B ) ` y ) , 0 ) ) e. MblFn )
60 53 56 59 mbfposr 
 |-  ( ( ph /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn ) ) -> ( y e. A |-> ( ( x e. A |-> B ) ` y ) ) e. MblFn )
61 51 60 eqeltrrd 
 |-  ( ( ph /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn ) ) -> ( x e. A |-> B ) e. MblFn )
62 50 61 impbida 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn <-> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn ) ) )