Theorem itg10

Description: The zero function has zero integral. (Contributed by Mario Carneiro, 18-Jun-2014)

	Ref	Expression
Assertion	itg10	$$⊢{\int }^1\left(ℝ\times \left\{0\right\}\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		i1f0	$$⊢ℝ\times \left\{0\right\}\in \mathrm{dom}{\int }^1$$
2		itg1val	$$⊢ℝ\times \left\{0\right\}\in \mathrm{dom}{\int }^1\to {\int }^1\left(ℝ\times \left\{0\right\}\right)=\sum _{x\in \mathrm{ran}\left(ℝ\times \left\{0\right\}\right)\setminus \left\{0\right\}}xvol\left({\left(ℝ\times \left\{0\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)$$
3	1 2	ax-mp	$$⊢{\int }^1\left(ℝ\times \left\{0\right\}\right)=\sum _{x\in \mathrm{ran}\left(ℝ\times \left\{0\right\}\right)\setminus \left\{0\right\}}xvol\left({\left(ℝ\times \left\{0\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)$$
4		rnxpss	$$⊢\mathrm{ran}\left(ℝ\times \left\{0\right\}\right)\subseteq \left\{0\right\}$$
5		ssdif0	$$⊢\mathrm{ran}\left(ℝ\times \left\{0\right\}\right)\subseteq \left\{0\right\}\leftrightarrow \mathrm{ran}\left(ℝ\times \left\{0\right\}\right)\setminus \left\{0\right\}=\varnothing$$
6	4 5	mpbi	$$⊢\mathrm{ran}\left(ℝ\times \left\{0\right\}\right)\setminus \left\{0\right\}=\varnothing$$
7	6	sumeq1i	$$⊢\sum _{x\in \mathrm{ran}\left(ℝ\times \left\{0\right\}\right)\setminus \left\{0\right\}}xvol\left({\left(ℝ\times \left\{0\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)=\sum _{x\in \varnothing }xvol\left({\left(ℝ\times \left\{0\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)$$
8		sum0	$$⊢\sum _{x\in \varnothing }xvol\left({\left(ℝ\times \left\{0\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)=0$$
9	3 7 8	3eqtri	$$⊢{\int }^1\left(ℝ\times \left\{0\right\}\right)=0$$