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 \in dom \int^{1} \to 0 \in ran F$

Proof

Step	Hyp	Ref	Expression
1		pnfnre	$⊢ +∞ \notin ℝ$
2	1	neli	$⊢ \neg +∞ \in ℝ$
3		rembl	$⊢ ℝ \in dom vol$
4		mblvol	$⊢ ℝ \in dom vol \to vol (ℝ) = {vol}^{*} (ℝ)$
5	3 4	ax-mp	$⊢ vol (ℝ) = {vol}^{*} (ℝ)$
6		ovolre	$⊢ {vol}^{*} (ℝ) = +∞$
7	5 6	eqtri	$⊢ vol (ℝ) = +∞$
8		cnvimarndm	$⊢ F^{-1} [ran F] = dom F$
9		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
10	9	fdmd	$⊢ F \in dom \int^{1} \to dom F = ℝ$
11	10	adantr	$⊢ (F \in dom \int^{1} \land \neg 0 \in ran F) \to dom F = ℝ$
12	8 11	syl5eq	$⊢ (F \in dom \int^{1} \land \neg 0 \in ran F) \to F^{-1} [ran F] = ℝ$
13	12	fveq2d	$⊢ (F \in dom \int^{1} \land \neg 0 \in ran F) \to vol (F^{-1} [ran F]) = vol (ℝ)$
14		i1fima2	$⊢ (F \in dom \int^{1} \land \neg 0 \in ran F) \to vol (F^{-1} [ran F]) \in ℝ$
15	13 14	eqeltrrd	$⊢ (F \in dom \int^{1} \land \neg 0 \in ran F) \to vol (ℝ) \in ℝ$
16	7 15	eqeltrrid	$⊢ (F \in dom \int^{1} \land \neg 0 \in ran F) \to +∞ \in ℝ$
17	16	ex	$⊢ F \in dom \int^{1} \to (\neg 0 \in ran F \to +∞ \in ℝ)$
18	2 17	mt3i	$⊢ F \in dom \int^{1} \to 0 \in ran F$