MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mbfposb Structured version   Visualization version   Unicode version

Theorem mbfposb 22657
Description: A function is measurable iff its positive and negative parts are measurable. (Contributed by Mario Carneiro, 11-Aug-2014.)
Hypothesis
Ref Expression
mbfpos.1  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  RR )
Assertion
Ref Expression
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 ) ) )
Distinct variable groups:    x, A    ph, x
Allowed substitution hint:    B( x)

Proof of Theorem mbfposb
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 nfcv 2602 . . . . . . . . 9  |-  F/_ x
0
2 nfcv 2602 . . . . . . . . 9  |-  F/_ x  <_
3 nffvmpt1 5895 . . . . . . . . 9  |-  F/_ x
( ( x  e.  A  |->  B ) `  y )
41, 2, 3nfbr 4460 . . . . . . . 8  |-  F/ x
0  <_  ( (
x  e.  A  |->  B ) `  y )
54, 3, 1nfif 3921 . . . . . . 7  |-  F/_ x if ( 0  <_  (
( x  e.  A  |->  B ) `  y
) ,  ( ( x  e.  A  |->  B ) `  y ) ,  0 )
6 nfcv 2602 . . . . . . 7  |-  F/_ y if ( 0  <_  (
( x  e.  A  |->  B ) `  x
) ,  ( ( x  e.  A  |->  B ) `  x ) ,  0 )
7 fveq2 5887 . . . . . . . . 9  |-  ( y  =  x  ->  (
( x  e.  A  |->  B ) `  y
)  =  ( ( x  e.  A  |->  B ) `  x ) )
87breq2d 4427 . . . . . . . 8  |-  ( y  =  x  ->  (
0  <_  ( (
x  e.  A  |->  B ) `  y )  <->  0  <_  ( (
x  e.  A  |->  B ) `  x ) ) )
98, 7ifbieq1d 3915 . . . . . . 7  |-  ( 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 ) )
105, 6, 9cbvmpt 4507 . . . . . 6  |-  ( 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 ) )
11 simpr 467 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
12 mbfpos.1 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  RR )
13 eqid 2461 . . . . . . . . . . 11  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
1413fvmpt2 5979 . . . . . . . . . 10  |-  ( ( x  e.  A  /\  B  e.  RR )  ->  ( ( x  e.  A  |->  B ) `  x )  =  B )
1511, 12, 14syl2anc 671 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  (
( x  e.  A  |->  B ) `  x
)  =  B )
1615breq2d 4427 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  (
0  <_  ( (
x  e.  A  |->  B ) `  x )  <->  0  <_  B )
)
1716, 15ifbieq1d 3915 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  if ( 0  <_  (
( x  e.  A  |->  B ) `  x
) ,  ( ( x  e.  A  |->  B ) `  x ) ,  0 )  =  if ( 0  <_  B ,  B , 
0 ) )
1817mpteq2dva 4502 . . . . . 6  |-  ( 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 ) ) )
1910, 18syl5eq 2507 . . . . 5  |-  ( 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 ) ) )
2019adantr 471 . . . 4  |-  ( (
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 ) ) )
2112, 13fmptd 6068 . . . . . . 7  |-  ( ph  ->  ( x  e.  A  |->  B ) : A --> RR )
2221adantr 471 . . . . . 6  |-  ( (
ph  /\  ( x  e.  A  |->  B )  e. MblFn )  ->  (
x  e.  A  |->  B ) : A --> RR )
2322ffvelrnda 6044 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  A  |->  B )  e. MblFn )  /\  y  e.  A )  ->  ( ( x  e.  A  |->  B ) `  y )  e.  RR )
24 nfcv 2602 . . . . . . . . 9  |-  F/_ y
( ( x  e.  A  |->  B ) `  x )
253, 24, 7cbvmpt 4507 . . . . . . . 8  |-  ( y  e.  A  |->  ( ( x  e.  A  |->  B ) `  y ) )  =  ( x  e.  A  |->  ( ( x  e.  A  |->  B ) `  x ) )
2615mpteq2dva 4502 . . . . . . . 8  |-  ( ph  ->  ( x  e.  A  |->  ( ( x  e.  A  |->  B ) `  x ) )  =  ( x  e.  A  |->  B ) )
2725, 26syl5eq 2507 . . . . . . 7  |-  ( ph  ->  ( y  e.  A  |->  ( ( x  e.  A  |->  B ) `  y ) )  =  ( x  e.  A  |->  B ) )
2827eleq1d 2523 . . . . . 6  |-  ( ph  ->  ( ( y  e.  A  |->  ( ( x  e.  A  |->  B ) `
 y ) )  e. MblFn 
<->  ( x  e.  A  |->  B )  e. MblFn )
)
2928biimpar 492 . . . . 5  |-  ( (
ph  /\  ( x  e.  A  |->  B )  e. MblFn )  ->  (
y  e.  A  |->  ( ( x  e.  A  |->  B ) `  y
) )  e. MblFn )
3023, 29mbfpos 22655 . . . 4  |-  ( (
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 )
3120, 30eqeltrrd 2540 . . 3  |-  ( (
ph  /\  ( x  e.  A  |->  B )  e. MblFn )  ->  (
x  e.  A  |->  if ( 0  <_  B ,  B ,  0 ) )  e. MblFn )
323nfneg 9896 . . . . . . . . 9  |-  F/_ x -u ( ( x  e.  A  |->  B ) `  y )
331, 2, 32nfbr 4460 . . . . . . . 8  |-  F/ x
0  <_  -u ( ( x  e.  A  |->  B ) `  y )
3433, 32, 1nfif 3921 . . . . . . 7  |-  F/_ x if ( 0  <_  -u (
( x  e.  A  |->  B ) `  y
) ,  -u (
( x  e.  A  |->  B ) `  y
) ,  0 )
35 nfcv 2602 . . . . . . 7  |-  F/_ y if ( 0  <_  -u (
( x  e.  A  |->  B ) `  x
) ,  -u (
( x  e.  A  |->  B ) `  x
) ,  0 )
367negeqd 9894 . . . . . . . . 9  |-  ( y  =  x  ->  -u (
( x  e.  A  |->  B ) `  y
)  =  -u (
( x  e.  A  |->  B ) `  x
) )
3736breq2d 4427 . . . . . . . 8  |-  ( y  =  x  ->  (
0  <_  -u ( ( x  e.  A  |->  B ) `  y )  <->  0  <_  -u ( ( x  e.  A  |->  B ) `  x ) ) )
3837, 36ifbieq1d 3915 . . . . . . 7  |-  ( 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 ) )
3934, 35, 38cbvmpt 4507 . . . . . 6  |-  ( 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 ) )
4015negeqd 9894 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  -u (
( x  e.  A  |->  B ) `  x
)  =  -u B
)
4140breq2d 4427 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  (
0  <_  -u ( ( x  e.  A  |->  B ) `  x )  <->  0  <_  -u B ) )
4241, 40ifbieq1d 3915 . . . . . . 7  |-  ( (
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 ) )
4342mpteq2dva 4502 . . . . . 6  |-  ( 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 ) ) )
4439, 43syl5eq 2507 . . . . 5  |-  ( 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 ) ) )
4544adantr 471 . . . 4  |-  ( (
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 ) ) )
4623renegcld 10073 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  A  |->  B )  e. MblFn )  /\  y  e.  A )  -> 
-u ( ( x  e.  A  |->  B ) `
 y )  e.  RR )
4723, 29mbfneg 22654 . . . . 5  |-  ( (
ph  /\  ( x  e.  A  |->  B )  e. MblFn )  ->  (
y  e.  A  |->  -u ( ( x  e.  A  |->  B ) `  y ) )  e. MblFn
)
4846, 47mbfpos 22655 . . . 4  |-  ( (
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 )
4945, 48eqeltrrd 2540 . . 3  |-  ( (
ph  /\  ( x  e.  A  |->  B )  e. MblFn )  ->  (
x  e.  A  |->  if ( 0  <_  -u B ,  -u B ,  0 ) )  e. MblFn )
5031, 49jca 539 . 2  |-  ( (
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 ) )
5127adantr 471 . . 3  |-  ( (
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 ) )
5221ffvelrnda 6044 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  (
( x  e.  A  |->  B ) `  y
)  e.  RR )
5352adantlr 726 . . . 4  |-  ( ( ( 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 )
5419adantr 471 . . . . 5  |-  ( (
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 769 . . . . 5  |-  ( (
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 )
5654, 55eqeltrd 2539 . . . 4  |-  ( (
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
)
5744adantr 471 . . . . 5  |-  ( (
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 771 . . . . 5  |-  ( (
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 )
5957, 58eqeltrd 2539 . . . 4  |-  ( (
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
)
6053, 56, 59mbfposr 22656 . . 3  |-  ( (
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 )
6151, 60eqeltrrd 2540 . 2  |-  ( (
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 )
6250, 61impbida 848 1  |-  ( 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 ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1454    e. wcel 1897   ifcif 3892   class class class wbr 4415    |-> cmpt 4474   -->wf 5596   ` cfv 5600   RRcr 9563   0cc0 9564    <_ cle 9701   -ucneg 9886  MblFncmbf 22620
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-inf2 8171  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641  ax-pre-sup 9642
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-fal 1460  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-int 4248  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-se 4812  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-isom 5609  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-of 6557  df-om 6719  df-1st 6819  df-2nd 6820  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-1o 7207  df-2o 7208  df-oadd 7211  df-er 7388  df-map 7499  df-pm 7500  df-en 7595  df-dom 7596  df-sdom 7597  df-fin 7598  df-sup 7981  df-inf 7982  df-oi 8050  df-card 8398  df-cda 8623  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-div 10297  df-nn 10637  df-2 10695  df-3 10696  df-n0 10898  df-z 10966  df-uz 11188  df-q 11293  df-rp 11331  df-xadd 11438  df-ioo 11667  df-ico 11669  df-icc 11670  df-fz 11813  df-fzo 11946  df-fl 12059  df-seq 12245  df-exp 12304  df-hash 12547  df-cj 13210  df-re 13211  df-im 13212  df-sqrt 13346  df-abs 13347  df-clim 13600  df-sum 13801  df-xmet 19011  df-met 19012  df-ovol 22464  df-vol 22466  df-mbf 22625
This theorem is referenced by:  iblre  22799
  Copyright terms: Public domain W3C validator