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

Metamath Proof Explorer

Theorem isi1f

Description: The predicate " F is a simple function". A simple function is a finite nonnegative linear combination of indicator functions for finitely measurable sets. We use the idiom F e. dom S.1 to represent this concept because S.1 is the first preparation function for our final definition S. (see df-itg ); unlike that operator, which can integrate any function, this operator can only integrate simple functions. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion isi1f ( 𝐹 ∈ dom ∫1 ↔ ( 𝐹 ∈ MblFn ∧ ( 𝐹 : ℝ ⟶ ℝ ∧ ran 𝐹 ∈ Fin ∧ ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) ) )

Proof

Step Hyp Ref Expression
1 feq1 ⊢ ( 𝑔 = 𝐹 → ( 𝑔 : ℝ ⟶ ℝ ↔ 𝐹 : ℝ ⟶ ℝ ) )
2 rneq ⊢ ( 𝑔 = 𝐹 → ran 𝑔 = ran 𝐹 )
3 2 eleq1d ⊢ ( 𝑔 = 𝐹 → ( ran 𝑔 ∈ Fin ↔ ran 𝐹 ∈ Fin ) )
4 cnveq ⊢ ( 𝑔 = 𝐹 → ◡ 𝑔 = ◡ 𝐹 )
5 4 imaeq1d ⊢ ( 𝑔 = 𝐹 → ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) = ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) )
6 5 fveq2d ⊢ ( 𝑔 = 𝐹 → ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) = ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) )
7 6 eleq1d ⊢ ( 𝑔 = 𝐹 → ( ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ↔ ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) )
8 1 3 7 3anbi123d ⊢ ( 𝑔 = 𝐹 → ( ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) ↔ ( 𝐹 : ℝ ⟶ ℝ ∧ ran 𝐹 ∈ Fin ∧ ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) ) )
9 sumex ⊢ Σ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ∈ V
10 df-itg1 ⊢ ∫1 = ( 𝑓 ∈ { 𝑔 ∈ MblFn ∣ ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) } ↦ Σ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) )
11 9 10 dmmpti ⊢ dom ∫1 = { 𝑔 ∈ MblFn ∣ ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) }
12 8 11 elrab2 ⊢ ( 𝐹 ∈ dom ∫1 ↔ ( 𝐹 ∈ MblFn ∧ ( 𝐹 : ℝ ⟶ ℝ ∧ ran 𝐹 ∈ Fin ∧ ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) ) )