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 ∖ 0 x ⁢ vol ⁡ f -1 x ∈ V
10 df-itg1 ⊢ ∫ 1 = f ∈ g ∈ MblFn | g : ℝ ⟶ ℝ ∧ ran ⁡ g ∈ Fin ∧ vol ⁡ g -1 ℝ ∖ 0 ∈ ℝ ⟼ ∑ x ∈ ran ⁡ f ∖ 0 x ⁢ vol ⁡ f -1 x
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 ∈ ℝ