Preamble: I suppose that the gist of this question is whether I've understood both the steps and what is reasonable to abstract away when using the standard machine to prove anything. In any case, one toy problem for the standard machine is the following:
Let $(\Omega, F, \mu)$ be a measure space, $A \in F$ and $F_A = \{A\cap B\mid B \in F\}$, and define the function $\mu_A[C] = \mu[A\cap B]$ for $C = A\cap B$ for some $B \in F$. Suppose that it is known that $F_A$ is a sigma-algebra, and that indeed $\mu_A$ is a measure. For any function $f:\Omega \to \mathbb{R}$ let $f|_A:A \to \mathbb{R}$ be its restriction to $A$.
Then, the straightforward way to show that $\int_A f|_Ad\mu_A = \int_\Omega 1_Afd\mu$ is by the standard machine, i.e. showing the equality for 1.) indicator functions, 2.) non-negative simple functions, 3.) non-negative measurable functions, 4.) all measurable functions $f$ s.t. $f|_A \in \mathcal{L}^1(\mu_A)$.
Question: Suppose that the equality has already been proven for indicator functions $f = 1_C, C \in F_A$, and the linearity $\int_A (af|_A + bg|_Ad)\mu_A = a\int_A f|_A\mu_A + b\int_Ag|_A\mu_A$ of such indicator functions has been confirmed.
Then question 1: is rest of the proof really just 2: invoking the linearity for a non-negative simple function, 3: using the monotone convergence theorem with an approximation sequence of non-negative simple functions to the non-negative measurable function, 4: splitting a general measurable function $f$ into its negative ($f_-$) and positive ($f_+$) component, and then applying to step 3.) and the measurability of $f$ to both $f_-$ and $f_+$ to finish the proof?
Question 2: Is it typical to prove the linearity at each step of the proof, or if the general results for integrals are known (like monotone/bounded convergence theorem) to be true, then do e.g. our restricted integral inherit there properties?
Best Answer
Question 1: Yes. This is exactly how you proceed. You use monotone convergence theorem to show that the two integrals coincide, then you use the canonical decomposition of a function in positive and negative part to lift it to the real case and if you want to go a step further you can split up in real part and complex part to obtain the result for complex functions.
Question 2: I don't understand your question here (what do you mean by vector space property?): once you proved that the restriction $(A, F_A, \mu_A)$ is a measure space, all the tools from measure theory become available.