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 )