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 eqtrid
 |-  ( ( 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 )