P. 235 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23401-23500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mbfimasn 23401	The preimage of a point under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( ( F e. MblFn /\ F : A --> RR /\ B e. RR ) -> ( `' F " { B } ) e. dom vol )
Theorem	mbfconst 23402	A constant function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
|- ( ( A e. dom vol /\ B e. CC ) -> ( A X. { B } ) e. MblFn )
Theorem	mbfid 23403	The identity function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
|- ( A e. dom vol -> ( _I |` A ) e. MblFn )
Theorem	mbfmptcl 23404*	Lemma for the MblFn predicate applied to a mapping operation. (Contributed by Mario Carneiro, 11-Aug-2014.)
|- ( ph -> ( x e. A |-> B ) e. MblFn )   &    |- ( ( ph /\ x e. A ) -> B e. V )   =>    |- ( ( ph /\ x e. A ) -> B e. CC )
Theorem	mbfdm2 23405*	The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Aug-2014.)
|- ( ph -> ( x e. A |-> B ) e. MblFn )   &    |- ( ( ph /\ x e. A ) -> B e. V )   =>    |- ( ph -> A e. dom vol )
Theorem	ismbfcn2 23406*	A complex function is measurable iff the real and imaginary components of the function are measurable. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. CC )   =>    |- ( ph -> ( ( x e. A |-> B ) e. MblFn <-> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) ) )
Theorem	ismbfd 23407*	Deduction to prove measurability of a real function. The third hypothesis is not necessary, but the proof of this requires countable choice, so we derive this separately as ismbf3d 23421. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( ph -> F : A --> RR )   &    |- ( ( ph /\ x e. RR* ) -> ( `' F " ( x (,) +oo ) ) e. dom vol )   &    |- ( ( ph /\ x e. RR* ) -> ( `' F " ( -oo (,) x ) ) e. dom vol )   =>    |- ( ph -> F e. MblFn )
Theorem	ismbf2d 23408*	Deduction to prove measurability of a real function. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( ph -> F : A --> RR )   &    |- ( ph -> A e. dom vol )   &    |- ( ( ph /\ x e. RR ) -> ( `' F " ( x (,) +oo ) ) e. dom vol )   &    |- ( ( ph /\ x e. RR ) -> ( `' F " ( -oo (,) x ) ) e. dom vol )   =>    |- ( ph -> F e. MblFn )
Theorem	mbfeqalem 23409*	Lemma for mbfeqa 23410. (Contributed by Mario Carneiro, 2-Sep-2014.)
|- ( ph -> A C_ RR )   &    |- ( ph -> ( vol* ` A ) = 0 )   &    |- ( ( ph /\ x e. ( B \ A ) ) -> C = D )   &    |- ( ( ph /\ x e. B ) -> C e. RR )   &    |- ( ( ph /\ x e. B ) -> D e. RR )   =>    |- ( ph -> ( ( x e. B |-> C ) e. MblFn <-> ( x e. B |-> D ) e. MblFn ) )
Theorem	mbfeqa 23410*	If two functions are equal almost everywhere, then one is measurable iff the other is. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 2-Sep-2014.)
|- ( ph -> A C_ RR )   &    |- ( ph -> ( vol* ` A ) = 0 )   &    |- ( ( ph /\ x e. ( B \ A ) ) -> C = D )   &    |- ( ( ph /\ x e. B ) -> C e. CC )   &    |- ( ( ph /\ x e. B ) -> D e. CC )   =>    |- ( ph -> ( ( x e. B |-> C ) e. MblFn <-> ( x e. B |-> D ) e. MblFn ) )
Theorem	mbfres 23411	The restriction of a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( ( F e. MblFn /\ A e. dom vol ) -> ( F |` A ) e. MblFn )
Theorem	mbfres2 23412	Measurability of a piecewise function: if F is measurable on subsets B and C of its domain, and these pieces make up all of A, then F is measurable on the whole domain. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( ph -> F : A --> RR )   &    |- ( ph -> ( F |` B ) e. MblFn )   &    |- ( ph -> ( F |` C ) e. MblFn )   &    |- ( ph -> ( B u. C ) = A )   =>    |- ( ph -> F e. MblFn )
Theorem	mbfss 23413*	Change the domain of a measurability predicate. (Contributed by Mario Carneiro, 17-Aug-2014.)
|- ( ph -> A C_ B )   &    |- ( ph -> B e. dom vol )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ( ph /\ x e. ( B \ A ) ) -> C = 0 )   &    |- ( ph -> ( x e. A |-> C ) e. MblFn )   =>    |- ( ph -> ( x e. B |-> C ) e. MblFn )
Theorem	mbfmulc2lem 23414	Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F : A --> RR )   =>    |- ( ph -> ( ( A X. { B } ) oF x. F ) e. MblFn )
Theorem	mbfmulc2re 23415	Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 15-Aug-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F : A --> CC )   =>    |- ( ph -> ( ( A X. { B } ) oF x. F ) e. MblFn )
Theorem	mbfmax 23416*	The maximum of two functions is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( ph -> F : A --> RR )   &    |- ( ph -> F e. MblFn )   &    |- ( ph -> G : A --> RR )   &    |- ( ph -> G e. MblFn )   &    |- H = ( x e. A |-> if ( ( F ` x ) <_ ( G ` x ) , ( G ` x ) , ( F ` x ) ) )   =>    |- ( ph -> H e. MblFn )
Theorem	mbfneg 23417*	The negative of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. MblFn )   =>    |- ( ph -> ( x e. A |-> -u B ) e. MblFn )
Theorem	mbfpos 23418*	The positive part of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.)
|- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. MblFn )   =>    |- ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
Theorem	mbfposr 23419*	Converse to mbfpos 23418. (Contributed by Mario Carneiro, 11-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )   &    |- ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn )   =>    |- ( ph -> ( x e. A |-> B ) e. MblFn )
Theorem	mbfposb 23420*	A function is measurable iff its positive and negative parts are measurable. (Contributed by Mario Carneiro, 11-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. RR )   =>    |- ( 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 ) ) )
Theorem	ismbf3d 23421*	Simplified form of ismbfd 23407. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( ph -> F : A --> RR )   &    |- ( ( ph /\ x e. RR ) -> ( `' F " ( x (,) +oo ) ) e. dom vol )   =>    |- ( ph -> F e. MblFn )
Theorem	mbfimaopnlem 23422*	Lemma for mbfimaopn 23423. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- J = ( TopOpen ` ℂfld )   &    |- G = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )   &    |- B = ( (,) " ( QQ X. QQ ) )   &    |- K = ran ( x e. B , y e. B |-> ( x X. y ) )   =>    |- ( ( F e. MblFn /\ A e. J ) -> ( `' F " A ) e. dom vol )
Theorem	mbfimaopn 23423	The preimage of any open set (in the complex topology) under a measurable function is measurable. (See also cncombf 23425, which explains why A e. dom vol is too weak a condition for this theorem.) (Contributed by Mario Carneiro, 25-Aug-2014.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( ( F e. MblFn /\ A e. J ) -> ( `' F " A ) e. dom vol )
Theorem	mbfimaopn2 23424	The preimage of any set open in the subspace topology of the range of the function is measurable. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t B )   =>    |- ( ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) /\ C e. K ) -> ( `' F " C ) e. dom vol )
Theorem	cncombf 23425	The composition of a continuous function with a measurable function is measurable. (More generally, G can be a Borel-measurable function, but notably the condition that G be only measurable is too weak, the usual counterexample taking G to be the Cantor function and F the indicator function of the G-image of a nonmeasurable set, which is a subset of the Cantor set and hence null and measurable.) (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> ( G o. F ) e. MblFn )
Theorem	cnmbf 23426	A continuous function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Mario Carneiro, 26-Mar-2015.)
|- ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) -> F e. MblFn )
Theorem	mbfaddlem 23427	The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> G e. MblFn )   &    |- ( ph -> F : A --> RR )   &    |- ( ph -> G : A --> RR )   =>    |- ( ph -> ( F oF + G ) e. MblFn )
Theorem	mbfadd 23428	The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> G e. MblFn )   =>    |- ( ph -> ( F oF + G ) e. MblFn )
Theorem	mbfsub 23429	The difference of two measurable functions is measurable. (Contributed by Mario Carneiro, 5-Sep-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> G e. MblFn )   =>    |- ( ph -> ( F oF - G ) e. MblFn )
Theorem	mbfmulc2 23430*	A complex constant times a measurable function is measurable. (Contributed by Mario Carneiro, 17-Aug-2014.)
|- ( ph -> C e. CC )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. MblFn )   =>    |- ( ph -> ( x e. A |-> ( C x. B ) ) e. MblFn )
Theorem	mbfsup 23431*	The supremum of a sequence of measurable, real-valued functions is measurable. Note that in this and related theorems, B ( n , x ) is a function of both n and x, since it is an n-indexed sequence of functions on x. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 7-Sep-2014.)
|- Z = ( ZZ>= ` M )   &    |- G = ( x e. A |-> sup ( ran ( n e. Z |-> B ) , RR , < ) )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. MblFn )   &    |- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> E. y e. RR A. n e. Z B <_ y )   =>    |- ( ph -> G e. MblFn )
Theorem	mbfinf 23432*	The infimum of a sequence of measurable, real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 13-Sep-2020.)
|- Z = ( ZZ>= ` M )   &    |- G = ( x e. A |-> inf ( ran ( n e. Z |-> B ) , RR , < ) )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. MblFn )   &    |- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> E. y e. RR A. n e. Z y <_ B )   =>    |- ( ph -> G e. MblFn )
Theorem	mbflimsup 23433*	The limit supremum of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.)
|- Z = ( ZZ>= ` M )   &    |- G = ( x e. A |-> ( limsup ` ( n e. Z |-> B ) ) )   &    |- H = ( m e. RR |-> sup ( ( ( ( n e. Z |-> B ) " ( m [,) +oo ) ) i^i RR* ) , RR* , < ) )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ x e. A ) -> ( limsup ` ( n e. Z |-> B ) ) e. RR )   &    |- ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. MblFn )   &    |- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. RR )   =>    |- ( ph -> G e. MblFn )
Theorem	mbflimlem 23434*	The pointwise limit of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) ~~> C )   &    |- ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. MblFn )   &    |- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. RR )   =>    |- ( ph -> ( x e. A |-> C ) e. MblFn )
Theorem	mbflim 23435*	The pointwise limit of a sequence of measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) ~~> C )   &    |- ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. MblFn )   &    |- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. V )   =>    |- ( ph -> ( x e. A |-> C ) e. MblFn )
Syntax	c0p 23436	Extend class notation to include the zero polynomial.
class 0p
Definition	df-0p 23437	Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.)
|- 0p = ( CC X. { 0 } )
Theorem	0pval 23438	The zero function evaluates to zero at every point. (Contributed by Mario Carneiro, 23-Jul-2014.)
|- ( A e. CC -> ( 0p ` A ) = 0 )
Theorem	0plef 23439	Two ways to say that the function F on the reals is nonnegative. (Contributed by Mario Carneiro, 17-Aug-2014.)
|- ( F : RR --> ( 0 [,) +oo ) <-> ( F : RR --> RR /\ 0p oR <_ F ) )
Theorem	0pledm 23440	Adjust the domain of the left argument to match the right, which works better in our theorems. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A C_ CC )   &    |- ( ph -> F Fn A )   =>    |- ( ph -> ( 0p oR <_ F <-> ( A X. { 0 } ) oR <_ F ) )
Theorem	isi1f 23441	The predicate " F is a simple function". A simple function is a finite nonnegative linear combination of indicator functions for finitely measurable sets. We use the idiom F e. dom S.1 to represent this concept because S.1 is the first preparation function for our final definition S. (see df-itg 23392); unlike that operator, which can integrate any function, this operator can only integrate simple functions. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( F e. dom S.1 <-> ( F e. MblFn /\ ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) )
Theorem	i1fmbf 23442	Simple functions are measurable. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( F e. dom S.1 -> F e. MblFn )
Theorem	i1ff 23443	A simple function is a function on the reals. (Contributed by Mario Carneiro, 26-Jun-2014.)
|- ( F e. dom S.1 -> F : RR --> RR )
Theorem	i1frn 23444	A simple function has finite range. (Contributed by Mario Carneiro, 26-Jun-2014.)
|- ( F e. dom S.1 -> ran F e. Fin )
Theorem	i1fima 23445	Any preimage of a simple function is measurable. (Contributed by Mario Carneiro, 26-Jun-2014.)
|- ( F e. dom S.1 -> ( `' F " A ) e. dom vol )
Theorem	i1fima2 23446	Any preimage of a simple function not containing zero has finite measure. (Contributed by Mario Carneiro, 26-Jun-2014.)
|- ( ( F e. dom S.1 /\ -. 0 e. A ) -> ( vol ` ( `' F " A ) ) e. RR )
Theorem	i1fima2sn 23447	Preimage of a singleton. (Contributed by Mario Carneiro, 26-Jun-2014.)
|- ( ( F e. dom S.1 /\ A e. ( B \ { 0 } ) ) -> ( vol ` ( `' F " { A } ) ) e. RR )
Theorem	i1fd 23448*	A simplified set of assumptions to show that a given function is simple. (Contributed by Mario Carneiro, 26-Jun-2014.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> ran F e. Fin )   &    |- ( ( ph /\ x e. ( ran F \ { 0 } ) ) -> ( `' F " { x } ) e. dom vol )   &    |- ( ( ph /\ x e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { x } ) ) e. RR )   =>    |- ( ph -> F e. dom S.1 )
Theorem	i1f0rn 23449	Any simple function takes the value zero on a set of unbounded measure, so in particular this set is not empty. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( F e. dom S.1 -> 0 e. ran F )
Theorem	itg1val 23450*	The value of the integral on simple functions. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( F e. dom S.1 -> ( S.1 ` F ) = sum_ x e. ( ran F \ { 0 } ) ( x x. ( vol ` ( `' F " { x } ) ) ) )
Theorem	itg1val2 23451*	The value of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014.)
|- ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) -> ( S.1 ` F ) = sum_ x e. A ( x x. ( vol ` ( `' F " { x } ) ) ) )
Theorem	itg1cl 23452	Closure of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014.)
|- ( F e. dom S.1 -> ( S.1 ` F ) e. RR )
Theorem	itg1ge0 23453	Closure of the integral on positive simple functions. (Contributed by Mario Carneiro, 19-Jun-2014.)
|- ( ( F e. dom S.1 /\ 0p oR <_ F ) -> 0 <_ ( S.1 ` F ) )
Theorem	i1f0 23454	The zero function is simple. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( RR X. { 0 } ) e. dom S.1
Theorem	itg10 23455	The zero function has zero integral. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( S.1 ` ( RR X. { 0 } ) ) = 0
Theorem	i1f1lem 23456*	Lemma for i1f1 23457 and itg11 23458. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- F = ( x e. RR |-> if ( x e. A , 1 , 0 ) )   =>    |- ( F : RR --> { 0 , 1 } /\ ( A e. dom vol -> ( `' F " { 1 } ) = A ) )
Theorem	i1f1 23457*	Base case simple functions are indicator functions of measurable sets. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- F = ( x e. RR |-> if ( x e. A , 1 , 0 ) )   =>    |- ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> F e. dom S.1 )
Theorem	itg11 23458*	The integral of an indicator function is the volume of the set. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- F = ( x e. RR |-> if ( x e. A , 1 , 0 ) )   =>    |- ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> ( S.1 ` F ) = ( vol ` A ) )
Theorem	itg1addlem1 23459*	Decompose a preimage, which is always a disjoint union. (Contributed by Mario Carneiro, 25-Jun-2014.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
|- ( ph -> F : X --> Y )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B C_ ( `' F " { k } ) )   &    |- ( ( ph /\ k e. A ) -> B e. dom vol )   &    |- ( ( ph /\ k e. A ) -> ( vol ` B ) e. RR )   =>    |- ( ph -> ( vol ` U_ k e. A B ) = sum_ k e. A ( vol ` B ) )
Theorem	i1faddlem 23460*	Decompose the preimage of a sum. (Contributed by Mario Carneiro, 19-Jun-2014.)
|- ( ph -> F e. dom S.1 )   &    |- ( ph -> G e. dom S.1 )   =>    |- ( ( ph /\ A e. CC ) -> ( `' ( F oF + G ) " { A } ) = U_ y e. ran G ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) )
Theorem	i1fmullem 23461*	Decompose the preimage of a product. (Contributed by Mario Carneiro, 19-Jun-2014.)
|- ( ph -> F e. dom S.1 )   &    |- ( ph -> G e. dom S.1 )   =>    |- ( ( ph /\ A e. ( CC \ { 0 } ) ) -> ( `' ( F oF x. G ) " { A } ) = U_ y e. ( ran G \ { 0 } ) ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) )
Theorem	i1fadd 23462	The sum of two simple functions is a simple function. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( ph -> F e. dom S.1 )   &    |- ( ph -> G e. dom S.1 )   =>    |- ( ph -> ( F oF + G ) e. dom S.1 )
Theorem	i1fmul 23463	The pointwise product of two simple functions is a simple function. (Contributed by Mario Carneiro, 5-Sep-2014.)
|- ( ph -> F e. dom S.1 )   &    |- ( ph -> G e. dom S.1 )   =>    |- ( ph -> ( F oF x. G ) e. dom S.1 )
Theorem	itg1addlem2 23464*	Lemma for itg1add 23468. The function I represents the pieces into which we will break up the domain of the sum. Since it is infinite only when both i and j are zero, we arbitrarily define it to be zero there to simplify the sums that are manipulated in itg1addlem4 23466 and itg1addlem5 23467. (Contributed by Mario Carneiro, 26-Jun-2014.)
|- ( ph -> F e. dom S.1 )   &    |- ( ph -> G e. dom S.1 )   &    |- I = ( i e. RR , j e. RR |-> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) )   =>    |- ( ph -> I : ( RR X. RR ) --> RR )
Theorem	itg1addlem3 23465*	Lemma for itg1add 23468. (Contributed by Mario Carneiro, 26-Jun-2014.)
|- ( ph -> F e. dom S.1 )   &    |- ( ph -> G e. dom S.1 )   &    |- I = ( i e. RR , j e. RR |-> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) )   =>    |- ( ( ( A e. RR /\ B e. RR ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( A I B ) = ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) )
Theorem	itg1addlem4 23466*	Lemma for itg1add . (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( ph -> F e. dom S.1 )   &    |- ( ph -> G e. dom S.1 )   &    |- I = ( i e. RR , j e. RR |-> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) )   &    |- P = ( + |` ( ran F X. ran G ) )   =>    |- ( ph -> ( S.1 ` ( F oF + G ) ) = sum_ y e. ran F sum_ z e. ran G ( ( y + z ) x. ( y I z ) ) )
Theorem	itg1addlem5 23467*	Lemma for itg1add . (Contributed by Mario Carneiro, 27-Jun-2014.)
|- ( ph -> F e. dom S.1 )   &    |- ( ph -> G e. dom S.1 )   &    |- I = ( i e. RR , j e. RR |-> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) )   &    |- P = ( + |` ( ran F X. ran G ) )   =>    |- ( ph -> ( S.1 ` ( F oF + G ) ) = ( ( S.1 ` F ) + ( S.1 ` G ) ) )
Theorem	itg1add 23468	The integral of a sum of simple functions is the sum of the integrals. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( ph -> F e. dom S.1 )   &    |- ( ph -> G e. dom S.1 )   =>    |- ( ph -> ( S.1 ` ( F oF + G ) ) = ( ( S.1 ` F ) + ( S.1 ` G ) ) )
Theorem	i1fmulclem 23469	Decompose the preimage of a constant times a function. (Contributed by Mario Carneiro, 25-Jun-2014.)
|- ( ph -> F e. dom S.1 )   &    |- ( ph -> A e. RR )   =>    |- ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( `' ( ( RR X. { A } ) oF x. F ) " { B } ) = ( `' F " { ( B / A ) } ) )
Theorem	i1fmulc 23470	A nonnegative constant times a simple function gives another simple function. (Contributed by Mario Carneiro, 25-Jun-2014.)
|- ( ph -> F e. dom S.1 )   &    |- ( ph -> A e. RR )   =>    |- ( ph -> ( ( RR X. { A } ) oF x. F ) e. dom S.1 )
Theorem	itg1mulc 23471	The integral of a constant times a simple function is the constant times the original integral. (Contributed by Mario Carneiro, 25-Jun-2014.)
|- ( ph -> F e. dom S.1 )   &    |- ( ph -> A e. RR )   =>    |- ( ph -> ( S.1 ` ( ( RR X. { A } ) oF x. F ) ) = ( A x. ( S.1 ` F ) ) )
Theorem	i1fres 23472*	The "restriction" of a simple function to a measurable subset is simple. (It's not actually a restriction because it is zero instead of undefined outside A.) (Contributed by Mario Carneiro, 29-Jun-2014.)
|- G = ( x e. RR |-> if ( x e. A , ( F ` x ) , 0 ) )   =>    |- ( ( F e. dom S.1 /\ A e. dom vol ) -> G e. dom S.1 )
Theorem	i1fpos 23473*	The positive part of a simple function is simple. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- G = ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) )   =>    |- ( F e. dom S.1 -> G e. dom S.1 )
Theorem	i1fposd 23474*	Deduction form of i1fposd 23474. (Contributed by Mario Carneiro, 6-Aug-2014.)
|- ( ph -> ( x e. RR |-> A ) e. dom S.1 )   =>    |- ( ph -> ( x e. RR |-> if ( 0 <_ A , A , 0 ) ) e. dom S.1 )
Theorem	i1fsub 23475	The difference of two simple functions is a simple function. (Contributed by Mario Carneiro, 6-Aug-2014.)
|- ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( F oF - G ) e. dom S.1 )
Theorem	itg1sub 23476	The integral of a difference of two simple functions. (Contributed by Mario Carneiro, 6-Aug-2014.)
|- ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( S.1 ` ( F oF - G ) ) = ( ( S.1 ` F ) - ( S.1 ` G ) ) )
Theorem	itg10a 23477*	The integral of a simple function supported on a nullset is zero. (Contributed by Mario Carneiro, 11-Aug-2014.)
|- ( ph -> F e. dom S.1 )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> ( vol* ` A ) = 0 )   &    |- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) = 0 )   =>    |- ( ph -> ( S.1 ` F ) = 0 )
Theorem	itg1ge0a 23478*	The integral of an almost positive simple function is positive. (Contributed by Mario Carneiro, 11-Aug-2014.)
|- ( ph -> F e. dom S.1 )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> ( vol* ` A ) = 0 )   &    |- ( ( ph /\ x e. ( RR \ A ) ) -> 0 <_ ( F ` x ) )   =>    |- ( ph -> 0 <_ ( S.1 ` F ) )
Theorem	itg1lea 23479*	Approximate version of itg1le 23480. If F <_ G for almost all x, then S.1 F <_ S.1 G. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 6-Aug-2014.)
|- ( ph -> F e. dom S.1 )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> ( vol* ` A ) = 0 )   &    |- ( ph -> G e. dom S.1 )   &    |- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) <_ ( G ` x ) )   =>    |- ( ph -> ( S.1 ` F ) <_ ( S.1 ` G ) )
Theorem	itg1le 23480	If one simple function dominates another, then the integral of the larger is also larger. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 6-Aug-2014.)
|- ( ( F e. dom S.1 /\ G e. dom S.1 /\ F oR <_ G ) -> ( S.1 ` F ) <_ ( S.1 ` G ) )
Theorem	itg1climres 23481*	Restricting the simple function F to the increasing sequence A ( n ) of measurable sets whose union is RR yields a sequence of simple functions whose integrals approach the integral of F. (Contributed by Mario Carneiro, 15-Aug-2014.)
|- ( ph -> A : NN --> dom vol )   &    |- ( ( ph /\ n e. NN ) -> ( A ` n ) C_ ( A ` ( n + 1 ) ) )   &    |- ( ph -> U. ran A = RR )   &    |- ( ph -> F e. dom S.1 )   &    |- G = ( x e. RR |-> if ( x e. ( A ` n ) , ( F ` x ) , 0 ) )   =>    |- ( ph -> ( n e. NN |-> ( S.1 ` G ) ) ~~> ( S.1 ` F ) )
Theorem	mbfi1fseqlem1 23482*	Lemma for mbfi1fseq 23488. (Contributed by Mario Carneiro, 16-Aug-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- J = ( m e. NN , y e. RR |-> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) )   =>    |- ( ph -> J : ( NN X. RR ) --> ( 0 [,) +oo ) )
Theorem	mbfi1fseqlem2 23483*	Lemma for mbfi1fseq 23488. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- J = ( m e. NN , y e. RR |-> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) )   &    |- G = ( m e. NN |-> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) )   =>    |- ( A e. NN -> ( G ` A ) = ( x e. RR |-> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) ) )
Theorem	mbfi1fseqlem3 23484*	Lemma for mbfi1fseq 23488. (Contributed by Mario Carneiro, 16-Aug-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- J = ( m e. NN , y e. RR |-> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) )   &    |- G = ( m e. NN |-> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) )   =>    |- ( ( ph /\ A e. NN ) -> ( G ` A ) : RR --> ran ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) )
Theorem	mbfi1fseqlem4 23485*	Lemma for mbfi1fseq 23488. This lemma is not as interesting as it is long - it is simply checking that G is in fact a sequence of simple functions, by verifying that its range is in ( 0 ... n 2 ^ n ) / ( 2 ^ n ) (which is to say, the numbers from 0 to n in increments of 1 / ( 2 ^ n )), and also that the preimage of each point k is measurable, because it is equal to ( -u n [,] n ) i^i ( `' F " ( k [,) k + 1 / ( 2 ^ n ) ) ) for k < n and ( -u n [,] n ) i^i ( `' F " ( k [,) +oo ) ) for k = n. (Contributed by Mario Carneiro, 16-Aug-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- J = ( m e. NN , y e. RR |-> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) )   &    |- G = ( m e. NN |-> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) )   =>    |- ( ph -> G : NN --> dom S.1 )
Theorem	mbfi1fseqlem5 23486*	Lemma for mbfi1fseq 23488. Verify that G describes an increasing sequence of positive functions. (Contributed by Mario Carneiro, 16-Aug-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- J = ( m e. NN , y e. RR |-> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) )   &    |- G = ( m e. NN |-> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) )   =>    |- ( ( ph /\ A e. NN ) -> ( 0p oR <_ ( G ` A ) /\ ( G ` A ) oR <_ ( G ` ( A + 1 ) ) ) )
Theorem	mbfi1fseqlem6 23487*	Lemma for mbfi1fseq 23488. Verify that G converges pointwise to F, and wrap up the existence quantifier. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- J = ( m e. NN , y e. RR |-> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) )   &    |- G = ( m e. NN |-> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) )   =>    |- ( 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 ) ) )
Theorem	mbfi1fseq 23488*	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.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> F : RR --> ( 0 [,) +oo ) )   =>    |- ( 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 ) ) )
Theorem	mbfi1flimlem 23489*	Lemma for mbfi1flim 23490. (Contributed by Mario Carneiro, 5-Sep-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> F : RR --> RR )   =>    |- ( ph -> E. g ( g : NN --> dom S.1 /\ A. x e. RR ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )
Theorem	mbfi1flim 23490*	Any real measurable function has a sequence of simple functions that converges to it. (Contributed by Mario Carneiro, 5-Sep-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> F : A --> RR )   =>    |- ( ph -> E. g ( g : NN --> dom S.1 /\ A. x e. A ( n e. NN |-> ( ( g ` n ) ` x ) ) ~~> ( F ` x ) ) )
Theorem	mbfmullem2 23491*	Lemma for mbfmul 23493. (Contributed by Mario Carneiro, 7-Sep-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> G e. MblFn )   &    |- ( ph -> F : A --> RR )   &    |- ( ph -> G : A --> RR )   &    |- ( ph -> P : NN --> dom S.1 )   &    |- ( ( ph /\ x e. A ) -> ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) )   &    |- ( ph -> Q : NN --> dom S.1 )   &    |- ( ( ph /\ x e. A ) -> ( n e. NN |-> ( ( Q ` n ) ` x ) ) ~~> ( G ` x ) )   =>    |- ( ph -> ( F oF x. G ) e. MblFn )
Theorem	mbfmullem 23492	Lemma for mbfmul 23493. (Contributed by Mario Carneiro, 7-Sep-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> G e. MblFn )   &    |- ( ph -> F : A --> RR )   &    |- ( ph -> G : A --> RR )   =>    |- ( ph -> ( F oF x. G ) e. MblFn )
Theorem	mbfmul 23493	The product of two measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> G e. MblFn )   =>    |- ( ph -> ( F oF x. G ) e. MblFn )
Theorem	itg2lcl 23494*	The set of lower sums is a set of extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- L = { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) }   =>    |- L C_ RR*
Theorem	itg2val 23495*	Value of the integral on nonnegative real functions. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- L = { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) }   =>    |- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) = sup ( L , RR* , < ) )
Theorem	itg2l 23496*	Elementhood in the set L of lower sums of the integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- L = { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) }   =>    |- ( A e. L <-> E. g e. dom S.1 ( g oR <_ F /\ A = ( S.1 ` g ) ) )
Theorem	itg2lr 23497*	Sufficient condition for elementhood in the set L. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- L = { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) }   =>    |- ( ( G e. dom S.1 /\ G oR <_ F ) -> ( S.1 ` G ) e. L )
Theorem	xrge0f 23498	A real function is a nonnegative extended real function if all its values are greater or equal to zero. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 28-Jul-2014.)
|- ( ( F : RR --> RR /\ 0p oR <_ F ) -> F : RR --> ( 0 [,] +oo ) )
Theorem	itg2cl 23499	The integral of a nonnegative real function is an extended real number. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* )
Theorem	itg2ub 23500	The integral of a nonnegative real function F is an upper bound on the integrals of all simple functions G dominated by F. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( ( F : RR --> ( 0 [,] +oo ) /\ G e. dom S.1 /\ G oR <_ F ) -> ( S.1 ` G ) <_ ( S.2 ` F ) )