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 = ( 𝑠 ∈ dom area ↦ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 )
2		areambl	⊢ ( ( 𝑠 ∈ dom area ∧ 𝑥 ∈ ℝ ) → ( ( 𝑠 “ { 𝑥 } ) ∈ dom vol ∧ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) ∈ ℝ ) )
3	2	simprd	⊢ ( ( 𝑠 ∈ dom area ∧ 𝑥 ∈ ℝ ) → ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) ∈ ℝ )
4		dmarea	⊢ ( 𝑠 ∈ dom area ↔ ( 𝑠 ⊆ ( ℝ × ℝ ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑠 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) )
5	4	simp3bi	⊢ ( 𝑠 ∈ dom area → ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) ) ∈ 𝐿1 )
6	3 5	itgrecl	⊢ ( 𝑠 ∈ dom area → ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 ∈ ℝ )
7	2	simpld	⊢ ( ( 𝑠 ∈ dom area ∧ 𝑥 ∈ ℝ ) → ( 𝑠 “ { 𝑥 } ) ∈ dom vol )
8		mblss	⊢ ( ( 𝑠 “ { 𝑥 } ) ∈ dom vol → ( 𝑠 “ { 𝑥 } ) ⊆ ℝ )
9		ovolge0	⊢ ( ( 𝑠 “ { 𝑥 } ) ⊆ ℝ → 0 ≤ ( vol* ‘ ( 𝑠 “ { 𝑥 } ) ) )
10	7 8 9	3syl	⊢ ( ( 𝑠 ∈ dom area ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( vol* ‘ ( 𝑠 “ { 𝑥 } ) ) )
11		mblvol	⊢ ( ( 𝑠 “ { 𝑥 } ) ∈ dom vol → ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) = ( vol* ‘ ( 𝑠 “ { 𝑥 } ) ) )
12	7 11	syl	⊢ ( ( 𝑠 ∈ dom area ∧ 𝑥 ∈ ℝ ) → ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) = ( vol* ‘ ( 𝑠 “ { 𝑥 } ) ) )
13	10 12	breqtrrd	⊢ ( ( 𝑠 ∈ dom area ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) )
14	5 3 13	itgge0	⊢ ( 𝑠 ∈ dom area → 0 ≤ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 )
15		elrege0	⊢ ( ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 ∈ ℝ ∧ 0 ≤ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 ) )
16	6 14 15	sylanbrc	⊢ ( 𝑠 ∈ dom area → ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 ∈ ( 0 [,) +∞ ) )
17	1 16	fmpti	⊢ area : dom area ⟶ ( 0 [,) +∞ )