Metamath Proof Explorer

Theorem i1f0rn

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

Ref Expression
Assertion i1f0rn 
|- ( F e. dom S.1 -> 0 e. ran F )

Proof

Step Hyp Ref Expression
1 pnfnre 
 |-  +oo e/ RR
2 1 neli 
 |-  -. +oo e. RR
3 rembl 
 |-  RR e. dom vol
4 mblvol 
 |-  ( RR e. dom vol -> ( vol ` RR ) = ( vol* ` RR ) )
5 3 4 ax-mp 
 |-  ( vol ` RR ) = ( vol* ` RR )
6 ovolre 
 |-  ( vol* ` RR ) = +oo
7 5 6 eqtri 
 |-  ( vol ` RR ) = +oo
8 cnvimarndm 
 |-  ( `' F " ran F ) = dom F
9 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
10 9 fdmd 
 |-  ( F e. dom S.1 -> dom F = RR )
11 10 adantr 
 |-  ( ( F e. dom S.1 /\ -. 0 e. ran F ) -> dom F = RR )
12 8 11 syl5eq 
 |-  ( ( F e. dom S.1 /\ -. 0 e. ran F ) -> ( `' F " ran F ) = RR )
13 12 fveq2d 
 |-  ( ( F e. dom S.1 /\ -. 0 e. ran F ) -> ( vol ` ( `' F " ran F ) ) = ( vol ` RR ) )
14 i1fima2 
 |-  ( ( F e. dom S.1 /\ -. 0 e. ran F ) -> ( vol ` ( `' F " ran F ) ) e. RR )
15 13 14 eqeltrrd 
 |-  ( ( F e. dom S.1 /\ -. 0 e. ran F ) -> ( vol ` RR ) e. RR )
16 7 15 eqeltrrid 
 |-  ( ( F e. dom S.1 /\ -. 0 e. ran F ) -> +oo e. RR )
17 16 ex 
 |-  ( F e. dom S.1 -> ( -. 0 e. ran F -> +oo e. RR ) )
18 2 17 mt3i 
 |-  ( F e. dom S.1 -> 0 e. ran F )