This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itg2ub

Description: 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)

Ref Expression
Assertion itg2ub 
|- ( ( F : RR --> ( 0 [,] +oo ) /\ G e. dom S.1 /\ G oR <_ F ) -> ( S.1 ` G ) <_ ( S.2 ` F ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } = { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) }
2 1 itg2lcl 
 |-  { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } C_ RR*
3 1 itg2lr 
 |-  ( ( G e. dom S.1 /\ G oR <_ F ) -> ( S.1 ` G ) e. { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } )
4 3 3adant1 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ G e. dom S.1 /\ G oR <_ F ) -> ( S.1 ` G ) e. { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } )
5 supxrub 
 |-  ( ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } C_ RR* /\ ( S.1 ` G ) e. { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } ) -> ( S.1 ` G ) <_ sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) )
6 2 4 5 sylancr 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ G e. dom S.1 /\ G oR <_ F ) -> ( S.1 ` G ) <_ sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) )
7 1 itg2val 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) = sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) )
8 7 3ad2ant1 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ G e. dom S.1 /\ G oR <_ F ) -> ( S.2 ` F ) = sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) )
9 6 8 breqtrrd 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ G e. dom S.1 /\ G oR <_ F ) -> ( S.1 ` G ) <_ ( S.2 ` F ) )