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, +∞)$

Step	Hyp	Ref	Expression
1		dfarea	$⊢ area = (s \in dom area ⟼ \int_{ℝ} vol (s [\{x\}]) d x)$
2		areambl	$⊢ (s \in dom area \land x \in ℝ) \to (s [\{x\}] \in dom vol \land vol (s [\{x\}]) \in ℝ)$
3	2	simprd	$⊢ (s \in dom area \land x \in ℝ) \to vol (s [\{x\}]) \in ℝ$
4		dmarea	$⊢ s \in dom area \leftrightarrow (s \subseteq ℝ^{2} \land \forall x \in ℝ s [\{x\}] \in {vol}^{-1} [ℝ] \land (x \in ℝ ⟼ vol (s [\{x\}])) \in 𝐿^{1})$
5	4	simp3bi	$⊢ s \in dom area \to (x \in ℝ ⟼ vol (s [\{x\}])) \in 𝐿^{1}$
6	3 5	itgrecl	$⊢ s \in dom area \to \int_{ℝ} vol (s [\{x\}]) d x \in ℝ$
7	2	simpld	$⊢ (s \in dom area \land x \in ℝ) \to s [\{x\}] \in dom vol$
8		mblss	$⊢ s [\{x\}] \in dom vol \to s [\{x\}] \subseteq ℝ$
9		ovolge0	$⊢ s [\{x\}] \subseteq ℝ \to 0 \leq {vol}^{*} (s [\{x\}])$
10	7 8 9	3syl	$⊢ (s \in dom area \land x \in ℝ) \to 0 \leq {vol}^{*} (s [\{x\}])$
11		mblvol	$⊢ s [\{x\}] \in dom vol \to vol (s [\{x\}]) = {vol}^{*} (s [\{x\}])$
12	7 11	syl	$⊢ (s \in dom area \land x \in ℝ) \to vol (s [\{x\}]) = {vol}^{*} (s [\{x\}])$
13	10 12	breqtrrd	$⊢ (s \in dom area \land x \in ℝ) \to 0 \leq vol (s [\{x\}])$
14	5 3 13	itgge0	$⊢ s \in dom area \to 0 \leq \int_{ℝ} vol (s [\{x\}]) d x$
15		elrege0	$⊢ \int_{ℝ} vol (s [\{x\}]) d x \in [0, +∞) \leftrightarrow (\int_{ℝ} vol (s [\{x\}]) d x \in ℝ \land 0 \leq \int_{ℝ} vol (s [\{x\}]) d x)$
16	6 14 15	sylanbrc	$⊢ s \in dom area \to \int_{ℝ} vol (s [\{x\}]) d x \in [0, +∞)$
17	1 16	fmpti	$⊢ area : dom area ⟶ [0, +∞)$

Metamath Proof Explorer