# 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}\in \mathrm{dom}{\int }^{1}↔\left({F}\in MblFn\wedge \left({F}:ℝ⟶ℝ\wedge \mathrm{ran}{F}\in \mathrm{Fin}\wedge vol\left({{F}}^{-1}\left[ℝ\setminus \left\{0\right\}\right]\right)\in ℝ\right)\right)$

### Proof

Step Hyp Ref Expression
1 feq1 ${⊢}{g}={F}\to \left({g}:ℝ⟶ℝ↔{F}:ℝ⟶ℝ\right)$
2 rneq ${⊢}{g}={F}\to \mathrm{ran}{g}=\mathrm{ran}{F}$
3 2 eleq1d ${⊢}{g}={F}\to \left(\mathrm{ran}{g}\in \mathrm{Fin}↔\mathrm{ran}{F}\in \mathrm{Fin}\right)$
4 cnveq ${⊢}{g}={F}\to {{g}}^{-1}={{F}}^{-1}$
5 4 imaeq1d ${⊢}{g}={F}\to {{g}}^{-1}\left[ℝ\setminus \left\{0\right\}\right]={{F}}^{-1}\left[ℝ\setminus \left\{0\right\}\right]$
6 5 fveq2d ${⊢}{g}={F}\to vol\left({{g}}^{-1}\left[ℝ\setminus \left\{0\right\}\right]\right)=vol\left({{F}}^{-1}\left[ℝ\setminus \left\{0\right\}\right]\right)$
7 6 eleq1d ${⊢}{g}={F}\to \left(vol\left({{g}}^{-1}\left[ℝ\setminus \left\{0\right\}\right]\right)\in ℝ↔vol\left({{F}}^{-1}\left[ℝ\setminus \left\{0\right\}\right]\right)\in ℝ\right)$
8 1 3 7 3anbi123d ${⊢}{g}={F}\to \left(\left({g}:ℝ⟶ℝ\wedge \mathrm{ran}{g}\in \mathrm{Fin}\wedge vol\left({{g}}^{-1}\left[ℝ\setminus \left\{0\right\}\right]\right)\in ℝ\right)↔\left({F}:ℝ⟶ℝ\wedge \mathrm{ran}{F}\in \mathrm{Fin}\wedge vol\left({{F}}^{-1}\left[ℝ\setminus \left\{0\right\}\right]\right)\in ℝ\right)\right)$
9 sumex ${⊢}\sum _{{x}\in \mathrm{ran}{f}\setminus \left\{0\right\}}{x}vol\left({{f}}^{-1}\left[\left\{{x}\right\}\right]\right)\in \mathrm{V}$
10 df-itg1 ${⊢}{\int }^{1}=\left({f}\in \left\{{g}\in MblFn|\left({g}:ℝ⟶ℝ\wedge \mathrm{ran}{g}\in \mathrm{Fin}\wedge vol\left({{g}}^{-1}\left[ℝ\setminus \left\{0\right\}\right]\right)\in ℝ\right)\right\}⟼\sum _{{x}\in \mathrm{ran}{f}\setminus \left\{0\right\}}{x}vol\left({{f}}^{-1}\left[\left\{{x}\right\}\right]\right)\right)$
11 9 10 dmmpti ${⊢}\mathrm{dom}{\int }^{1}=\left\{{g}\in MblFn|\left({g}:ℝ⟶ℝ\wedge \mathrm{ran}{g}\in \mathrm{Fin}\wedge vol\left({{g}}^{-1}\left[ℝ\setminus \left\{0\right\}\right]\right)\in ℝ\right)\right\}$
12 8 11 elrab2 ${⊢}{F}\in \mathrm{dom}{\int }^{1}↔\left({F}\in MblFn\wedge \left({F}:ℝ⟶ℝ\wedge \mathrm{ran}{F}\in \mathrm{Fin}\wedge vol\left({{F}}^{-1}\left[ℝ\setminus \left\{0\right\}\right]\right)\in ℝ\right)\right)$