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 ⊢F∈dom⁡∫1↔F∈MblFn∧F:ℝ⟶ℝ∧ran⁡F∈Fin∧vol⁡F-1ℝ∖0∈ℝ

Proof

Step Hyp Ref Expression
1 feq1 ⊢g=F→g:ℝ⟶ℝ↔F:ℝ⟶ℝ
2 rneq ⊢g=F→ran⁡g=ran⁡F
3 2 eleq1d ⊢g=F→ran⁡g∈Fin↔ran⁡F∈Fin
4 cnveq ⊢g=F→g-1=F-1
5 4 imaeq1d ⊢g=F→g-1ℝ∖0=F-1ℝ∖0
6 5 fveq2d ⊢g=F→vol⁡g-1ℝ∖0=vol⁡F-1ℝ∖0
7 6 eleq1d ⊢g=F→vol⁡g-1ℝ∖0∈ℝ↔vol⁡F-1ℝ∖0∈ℝ
8 1 3 7 3anbi123d ⊢g=F→g:ℝ⟶ℝ∧ran⁡g∈Fin∧vol⁡g-1ℝ∖0∈ℝ↔F:ℝ⟶ℝ∧ran⁡F∈Fin∧vol⁡F-1ℝ∖0∈ℝ
9 sumex ⊢∑x∈ran⁡f∖0x⁢vol⁡f-1x∈V
10 df-itg1 ⊢∫1=f∈g∈MblFn|g:ℝ⟶ℝ∧ran⁡g∈Fin∧vol⁡g-1ℝ∖0∈ℝ⟼∑x∈ran⁡f∖0x⁢vol⁡f-1x
11 9 10 dmmpti ⊢dom⁡∫1=g∈MblFn|g:ℝ⟶ℝ∧ran⁡g∈Fin∧vol⁡g-1ℝ∖0∈ℝ
12 8 11 elrab2 ⊢F∈dom⁡∫1↔F∈MblFn∧F:ℝ⟶ℝ∧ran⁡F∈Fin∧vol⁡F-1ℝ∖0∈ℝ