ThmDex – An index of mathematical definitions, results, and conjectures.
P2463
Let $\phi$ be a measurable simple function on $M$ such that $0 \leq \phi \leq f I_E$. Now $\phi = \phi I_E$. Let $\sum_{n = 1}^N a_n I_{E_n}$ be a D1745: Standard simple function representation of $\phi I_E$. Since $\phi I_E$ is nonzero only on $E$, then $a_n \neq 0$ only for those $E_n$ for which $E_n \subseteq E$. Since $E_1, \dots, E_N$ are measurable (being part of the standard representation), result R3513: Measurable subnull set has measure zero shows that $\mu(E_1) = \cdots = \mu(E_N) = 0$. Thus \begin{equation} \int_X \phi \, d \mu = \int_X \phi I_E \, d \mu : = \sum_{n = 1}^N a_n \mu(E_n) = 0 \end{equation} We may now take supremums on each side over all measurable simple functions $0 \leq \phi \leq f I_E$ to obtain \begin{equation} \int_E f \, d \mu : = \sup_{0 \leq \phi \leq f I_E, \, \phi \text{ measurable and simple}} \int_X \phi \, d \mu = 0 \end{equation} $\square$