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 ( 𝐹 ∈ dom ∫1 → 0 ∈ ran 𝐹 )

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 ⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹
9 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
10 9 fdmd ⊢ ( 𝐹 ∈ dom ∫1 → dom 𝐹 = ℝ )
11 10 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ ran 𝐹 ) → dom 𝐹 = ℝ )
12 8 11 eqtrid ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ ran 𝐹 ) → ( ◡ 𝐹 “ ran 𝐹 ) = ℝ )
13 12 fveq2d ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ ran 𝐹 ) → ( vol ‘ ( ◡ 𝐹 “ ran 𝐹 ) ) = ( vol ‘ ℝ ) )
14 i1fima2 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ ran 𝐹 ) → ( vol ‘ ( ◡ 𝐹 “ ran 𝐹 ) ) ∈ ℝ )
15 13 14 eqeltrrd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ ran 𝐹 ) → ( vol ‘ ℝ ) ∈ ℝ )
16 7 15 eqeltrrid ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ ran 𝐹 ) → +∞ ∈ ℝ )
17 16 ex ⊢ ( 𝐹 ∈ dom ∫1 → ( ¬ 0 ∈ ran 𝐹 → +∞ ∈ ℝ ) )
18 2 17 mt3i ⊢ ( 𝐹 ∈ dom ∫1 → 0 ∈ ran 𝐹 )