Theorem itg1add

Description: The integral of a sum of simple functions is the sum of the integrals. (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Hypotheses	i1fadd.1	$$⊢\phi \to F\in \mathrm{dom}{\int }^1$$
	i1fadd.2	$$⊢\phi \to G\in \mathrm{dom}{\int }^1$$
Assertion	itg1add	$$⊢\phi \to {\int }^1\left(F{+}_{f}G\right)={\int }^1\left(F\right)+{\int }^1\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		i1fadd.1	$$⊢\phi \to F\in \mathrm{dom}{\int }^1$$
2		i1fadd.2	$$⊢\phi \to G\in \mathrm{dom}{\int }^1$$
3		eqid	$$⊢\left(i\in ℝ,j\in ℝ⟼if\left(\left(i=0\wedge j=0\right),0,vol\left(F^{-1}\left[\left\{i\right\}\right]\cap G^{-1}\left[\left\{j\right\}\right]\right)\right)\right)=\left(i\in ℝ,j\in ℝ⟼if\left(\left(i=0\wedge j=0\right),0,vol\left(F^{-1}\left[\left\{i\right\}\right]\cap G^{-1}\left[\left\{j\right\}\right]\right)\right)\right)$$
4		eqid	$$⊢{+\upharpoonright }_{\left(\mathrm{ran}F\times \mathrm{ran}G\right)}={+\upharpoonright }_{\left(\mathrm{ran}F\times \mathrm{ran}G\right)}$$
5	1 2 3 4	itg1addlem5	$$⊢\phi \to {\int }^1\left(F{+}_{f}G\right)={\int }^1\left(F\right)+{\int }^1\left(G\right)$$