This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐹 ) ∈ ℝ )