Metamath Proof Explorer

Theorem areaf

Description: Area measurement is a function whose values are nonnegative reals. (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion areaf ⊢ area : dom ⁡ area ⟶ 0 +∞

Proof

Step Hyp Ref Expression
1 dfarea ⊢ area = s ∈ dom ⁡ area ⟼ ∫ ℝ vol ⁡ s x dx
2 areambl ⊢ s ∈ dom ⁡ area ∧ x ∈ ℝ → s x ∈ dom ⁡ vol ∧ vol ⁡ s x ∈ ℝ
3 2 simprd ⊢ s ∈ dom ⁡ area ∧ x ∈ ℝ → vol ⁡ s x ∈ ℝ
4 dmarea ⊢ s ∈ dom ⁡ area ↔ s ⊆ ℝ 2 ∧ ∀ x ∈ ℝ s x ∈ vol -1 ℝ ∧ x ∈ ℝ ⟼ vol ⁡ s x ∈ 𝐿 1
5 4 simp3bi ⊢ s ∈ dom ⁡ area → x ∈ ℝ ⟼ vol ⁡ s x ∈ 𝐿 1
6 3 5 itgrecl ⊢ s ∈ dom ⁡ area → ∫ ℝ vol ⁡ s x dx ∈ ℝ
7 2 simpld ⊢ s ∈ dom ⁡ area ∧ x ∈ ℝ → s x ∈ dom ⁡ vol
8 mblss ⊢ s x ∈ dom ⁡ vol → s x ⊆ ℝ
9 ovolge0 ⊢ s x ⊆ ℝ → 0 ≤ vol * ⁡ s x
10 7 8 9 3syl ⊢ s ∈ dom ⁡ area ∧ x ∈ ℝ → 0 ≤ vol * ⁡ s x
11 mblvol ⊢ s x ∈ dom ⁡ vol → vol ⁡ s x = vol * ⁡ s x
12 7 11 syl ⊢ s ∈ dom ⁡ area ∧ x ∈ ℝ → vol ⁡ s x = vol * ⁡ s x
13 10 12 breqtrrd ⊢ s ∈ dom ⁡ area ∧ x ∈ ℝ → 0 ≤ vol ⁡ s x
14 5 3 13 itgge0 ⊢ s ∈ dom ⁡ area → 0 ≤ ∫ ℝ vol ⁡ s x dx
15 elrege0 ⊢ ∫ ℝ vol ⁡ s x dx ∈ 0 +∞ ↔ ∫ ℝ vol ⁡ s x dx ∈ ℝ ∧ 0 ≤ ∫ ℝ vol ⁡ s x dx
16 6 14 15 sylanbrc ⊢ s ∈ dom ⁡ area → ∫ ℝ vol ⁡ s x dx ∈ 0 +∞
17 1 16 fmpti ⊢ area : dom ⁡ area ⟶ 0 +∞