Theorem itg1cl

Description: Closure of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014)

	Ref	Expression
Assertion	itg1cl	⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		itg1val	⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) = Σ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) )
2		i1frn	⊢ ( 𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin )
3		difss	⊢ ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹
4		ssfi	⊢ ( ( ran 𝐹 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹 ) → ( ran 𝐹 ∖ { 0 } ) ∈ Fin )
5	2 3 4	sylancl	⊢ ( 𝐹 ∈ dom ∫1 → ( ran 𝐹 ∖ { 0 } ) ∈ Fin )
6		i1ff	⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
7	6	frnd	⊢ ( 𝐹 ∈ dom ∫1 → ran 𝐹 ⊆ ℝ )
8	7	ssdifssd	⊢ ( 𝐹 ∈ dom ∫1 → ( ran 𝐹 ∖ { 0 } ) ⊆ ℝ )
9	8	sselda	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝑥 ∈ ℝ )
10		i1fima2sn	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ )
11	9 10	remulcld	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ℝ )
12	5 11	fsumrecl	⊢ ( 𝐹 ∈ dom ∫1 → Σ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ℝ )
13	1 12	eqeltrd	⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) ∈ ℝ )