Theorem areaval

Description: The area of a measurable region is greater than or equal to zero. (Contributed by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Assertion	areaval	$$⊢S\in \mathrm{dom}area\to area\left(S\right)={\int }_{ℝ}vol\left(S\left[\left\{x\right\}\right]\right)dx$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(s=S\wedge x\in ℝ\right)\to s=S$$
2	1	imaeq1d	$$⊢\left(s=S\wedge x\in ℝ\right)\to s\left[\left\{x\right\}\right]=S\left[\left\{x\right\}\right]$$
3	2	fveq2d	$$⊢\left(s=S\wedge x\in ℝ\right)\to vol\left(s\left[\left\{x\right\}\right]\right)=vol\left(S\left[\left\{x\right\}\right]\right)$$
4	3	itgeq2dv	$$⊢s=S\to {\int }_{ℝ}vol\left(s\left[\left\{x\right\}\right]\right)dx={\int }_{ℝ}vol\left(S\left[\left\{x\right\}\right]\right)dx$$
5		dfarea	$$⊢area=\left(s\in \mathrm{dom}area⟼{\int }_{ℝ}vol\left(s\left[\left\{x\right\}\right]\right)dx\right)$$
6		itgex	$$⊢{\int }_{ℝ}vol\left(S\left[\left\{x\right\}\right]\right)dx\in \mathrm{V}$$
7	4 5 6	fvmpt	$$⊢S\in \mathrm{dom}area\to area\left(S\right)={\int }_{ℝ}vol\left(S\left[\left\{x\right\}\right]\right)dx$$