This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ dom ⁡ ∫ 1 → 0 ∈ ran ⁡ F

Proof

Step Hyp Ref Expression
1 pnfnre ⊢ +∞ ∉ ℝ
2 1 neli ⊢ ¬ +∞ ∈ ℝ
3 rembl ⊢ ℝ ∈ dom ⁡ vol
4 mblvol ⊢ ℝ ∈ dom ⁡ vol → 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 ∈ dom ⁡ ∫ 1 → F : ℝ ⟶ ℝ
10 9 fdmd ⊢ F ∈ dom ⁡ ∫ 1 → dom ⁡ F = ℝ
11 10 adantr ⊢ F ∈ dom ⁡ ∫ 1 ∧ ¬ 0 ∈ ran ⁡ F → dom ⁡ F = ℝ
12 8 11 eqtrid ⊢ F ∈ dom ⁡ ∫ 1 ∧ ¬ 0 ∈ ran ⁡ F → F -1 ran ⁡ F = ℝ
13 12 fveq2d ⊢ F ∈ dom ⁡ ∫ 1 ∧ ¬ 0 ∈ ran ⁡ F → vol ⁡ F -1 ran ⁡ F = vol ⁡ ℝ
14 i1fima2 ⊢ F ∈ dom ⁡ ∫ 1 ∧ ¬ 0 ∈ ran ⁡ F → vol ⁡ F -1 ran ⁡ F ∈ ℝ
15 13 14 eqeltrrd ⊢ F ∈ dom ⁡ ∫ 1 ∧ ¬ 0 ∈ ran ⁡ F → vol ⁡ ℝ ∈ ℝ
16 7 15 eqeltrrid ⊢ F ∈ dom ⁡ ∫ 1 ∧ ¬ 0 ∈ ran ⁡ F → +∞ ∈ ℝ
17 16 ex ⊢ F ∈ dom ⁡ ∫ 1 → ¬ 0 ∈ ran ⁡ F → +∞ ∈ ℝ
18 2 17 mt3i ⊢ F ∈ dom ⁡ ∫ 1 → 0 ∈ ran ⁡ F