Metamath Proof Explorer

Theorem mbfi1fseq

Description: A characterization of measurability in terms of simple functions (this is an if and only if for nonnegative functions, although we don't prove it). Any nonnegative measurable function is the limit of an increasing sequence of nonnegative simple functions. This proof is an example of a poor de Bruijn factor - the formalized proof is much longer than an average hand proof, which usually just describes the function G and "leaves the details as an exercise to the reader". (Contributed by Mario Carneiro, 16-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses mbfi1fseq.1 
|- ( ph -> F e. MblFn )
mbfi1fseq.2 
|- ( ph -> F : RR --> ( 0 [,) +oo ) )
Assertion mbfi1fseq 
|- ( ph -> E. g ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )

Proof

Step Hyp Ref Expression
1 mbfi1fseq.1 
 |-  ( ph -> F e. MblFn )
2 mbfi1fseq.2 
 |-  ( ph -> F : RR --> ( 0 [,) +oo ) )
3 oveq2 
 |-  ( j = k -> ( 2 ^ j ) = ( 2 ^ k ) )
4 3 oveq2d 
 |-  ( j = k -> ( ( F ` z ) x. ( 2 ^ j ) ) = ( ( F ` z ) x. ( 2 ^ k ) ) )
5 4 fveq2d 
 |-  ( j = k -> ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) = ( |_ ` ( ( F ` z ) x. ( 2 ^ k ) ) ) )
6 5 3 oveq12d 
 |-  ( j = k -> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) = ( ( |_ ` ( ( F ` z ) x. ( 2 ^ k ) ) ) / ( 2 ^ k ) ) )
7 fveq2 
 |-  ( z = y -> ( F ` z ) = ( F ` y ) )
8 7 fvoveq1d 
 |-  ( z = y -> ( |_ ` ( ( F ` z ) x. ( 2 ^ k ) ) ) = ( |_ ` ( ( F ` y ) x. ( 2 ^ k ) ) ) )
9 8 oveq1d 
 |-  ( z = y -> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ k ) ) ) / ( 2 ^ k ) ) = ( ( |_ ` ( ( F ` y ) x. ( 2 ^ k ) ) ) / ( 2 ^ k ) ) )
10 6 9 cbvmpov 
 |-  ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) = ( k e. NN , y e. RR |-> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ k ) ) ) / ( 2 ^ k ) ) )
11 eleq1w 
 |-  ( y = x -> ( y e. ( -u m [,] m ) <-> x e. ( -u m [,] m ) ) )
12 oveq2 
 |-  ( y = x -> ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) y ) = ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) )
13 12 breq1d 
 |-  ( y = x -> ( ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) y ) <_ m <-> ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) <_ m ) )
14 13 12 ifbieq1d 
 |-  ( y = x -> if ( ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) y ) <_ m , ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) y ) , m ) = if ( ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) <_ m , ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) , m ) )
15 11 14 ifbieq1d 
 |-  ( y = x -> if ( y e. ( -u m [,] m ) , if ( ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) y ) <_ m , ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) y ) , m ) , 0 ) = if ( x e. ( -u m [,] m ) , if ( ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) <_ m , ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) , m ) , 0 ) )
16 15 cbvmptv 
 |-  ( y e. RR |-> if ( y e. ( -u m [,] m ) , if ( ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) y ) <_ m , ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) y ) , m ) , 0 ) ) = ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) <_ m , ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) , m ) , 0 ) )
17 negeq 
 |-  ( m = k -> -u m = -u k )
18 id 
 |-  ( m = k -> m = k )
19 17 18 oveq12d 
 |-  ( m = k -> ( -u m [,] m ) = ( -u k [,] k ) )
20 19 eleq2d 
 |-  ( m = k -> ( x e. ( -u m [,] m ) <-> x e. ( -u k [,] k ) ) )
21 oveq1 
 |-  ( m = k -> ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) = ( k ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) )
22 21 18 breq12d 
 |-  ( m = k -> ( ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) <_ m <-> ( k ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) <_ k ) )
23 22 21 18 ifbieq12d 
 |-  ( m = k -> if ( ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) <_ m , ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) , m ) = if ( ( k ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) <_ k , ( k ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) , k ) )
24 20 23 ifbieq1d 
 |-  ( m = k -> if ( x e. ( -u m [,] m ) , if ( ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) <_ m , ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) , m ) , 0 ) = if ( x e. ( -u k [,] k ) , if ( ( k ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) <_ k , ( k ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) , k ) , 0 ) )
25 24 mpteq2dv 
 |-  ( m = k -> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) <_ m , ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) , m ) , 0 ) ) = ( x e. RR |-> if ( x e. ( -u k [,] k ) , if ( ( k ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) <_ k , ( k ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) , k ) , 0 ) ) )
26 16 25 syl5eq 
 |-  ( m = k -> ( y e. RR |-> if ( y e. ( -u m [,] m ) , if ( ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) y ) <_ m , ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) y ) , m ) , 0 ) ) = ( x e. RR |-> if ( x e. ( -u k [,] k ) , if ( ( k ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) <_ k , ( k ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) , k ) , 0 ) ) )
27 26 cbvmptv 
 |-  ( m e. NN |-> ( y e. RR |-> if ( y e. ( -u m [,] m ) , if ( ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) y ) <_ m , ( m ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) y ) , m ) , 0 ) ) ) = ( k e. NN |-> ( x e. RR |-> if ( x e. ( -u k [,] k ) , if ( ( k ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) <_ k , ( k ( j e. NN , z e. RR |-> ( ( |_ ` ( ( F ` z ) x. ( 2 ^ j ) ) ) / ( 2 ^ j ) ) ) x ) , k ) , 0 ) ) )
28 1 2 10 27 mbfi1fseqlem6 
 |-  ( ph -> E. g ( g : NN --> dom S.1 /\ A. n e. NN ( 0p oR <_ ( g ` n ) /\ ( g ` n ) oR <_ ( g ` ( n + 1 ) ) ) /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )