Metamath Proof Explorer

Theorem areaf

Description: Area measurement is a function whose values are nonnegative reals. (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion areaf 
|- area : dom area --> ( 0 [,) +oo )

Proof

Step Hyp Ref Expression
1 dfarea 
 |-  area = ( s e. dom area |-> S. RR ( vol ` ( s " { x } ) ) _d x )
2 areambl 
 |-  ( ( s e. dom area /\ x e. RR ) -> ( ( s " { x } ) e. dom vol /\ ( vol ` ( s " { x } ) ) e. RR ) )
3 2 simprd 
 |-  ( ( s e. dom area /\ x e. RR ) -> ( vol ` ( s " { x } ) ) e. RR )
4 dmarea 
 |-  ( s e. dom area <-> ( s C_ ( RR X. RR ) /\ A. x e. RR ( s " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( s " { x } ) ) ) e. L^1 ) )
5 4 simp3bi 
 |-  ( s e. dom area -> ( x e. RR |-> ( vol ` ( s " { x } ) ) ) e. L^1 )
6 3 5 itgrecl 
 |-  ( s e. dom area -> S. RR ( vol ` ( s " { x } ) ) _d x e. RR )
7 2 simpld 
 |-  ( ( s e. dom area /\ x e. RR ) -> ( s " { x } ) e. dom vol )
8 mblss 
 |-  ( ( s " { x } ) e. dom vol -> ( s " { x } ) C_ RR )
9 ovolge0 
 |-  ( ( s " { x } ) C_ RR -> 0 <_ ( vol* ` ( s " { x } ) ) )
10 7 8 9 3syl 
 |-  ( ( s e. dom area /\ x e. RR ) -> 0 <_ ( vol* ` ( s " { x } ) ) )
11 mblvol 
 |-  ( ( s " { x } ) e. dom vol -> ( vol ` ( s " { x } ) ) = ( vol* ` ( s " { x } ) ) )
12 7 11 syl 
 |-  ( ( s e. dom area /\ x e. RR ) -> ( vol ` ( s " { x } ) ) = ( vol* ` ( s " { x } ) ) )
13 10 12 breqtrrd 
 |-  ( ( s e. dom area /\ x e. RR ) -> 0 <_ ( vol ` ( s " { x } ) ) )
14 5 3 13 itgge0 
 |-  ( s e. dom area -> 0 <_ S. RR ( vol ` ( s " { x } ) ) _d x )
15 elrege0 
 |-  ( S. RR ( vol ` ( s " { x } ) ) _d x e. ( 0 [,) +oo ) <-> ( S. RR ( vol ` ( s " { x } ) ) _d x e. RR /\ 0 <_ S. RR ( vol ` ( s " { x } ) ) _d x ) )
16 6 14 15 sylanbrc 
 |-  ( s e. dom area -> S. RR ( vol ` ( s " { x } ) ) _d x e. ( 0 [,) +oo ) )
17 1 16 fmpti 
 |-  area : dom area --> ( 0 [,) +oo )