Theorem sitg0

Description: The integral of the constant zero function is zero. (Contributed by Thierry Arnoux, 13-Mar-2018)

	Ref	Expression
Hypotheses	sitgval.b	$$⊢B={\mathrm{Base}}_W$$
	sitgval.j	$$⊢J=\mathrm{TopOpen}\left(W\right)$$
	sitgval.s	$$⊢S=𝛔\left(J\right)$$
	sitgval.0	$$⊢\underset{\dot{}}{0}=0_W$$
	sitgval.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	sitgval.h	$$⊢H=\mathrm{ℝHom}\left(\mathrm{Scalar}\left(W\right)\right)$$
	sitgval.1	$$⊢\phi \to W\in V$$
	sitgval.2	$$⊢\phi \to M\in \bigcup \mathrm{ran}\mathrm{measures}$$
	sitg0.1	$$⊢\phi \to W\in \mathrm{TopSp}$$
	sitg0.2	$$⊢\phi \to W\in \mathrm{Mnd}$$
Assertion	sitg0	$$⊢\phi \to {\int }_{\Im }^W\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)dM=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	$$⊢B={\mathrm{Base}}_W$$
2		sitgval.j	$$⊢J=\mathrm{TopOpen}\left(W\right)$$
3		sitgval.s	$$⊢S=𝛔\left(J\right)$$
4		sitgval.0	$$⊢\underset{\dot{}}{0}=0_W$$
5		sitgval.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		sitgval.h	$$⊢H=\mathrm{ℝHom}\left(\mathrm{Scalar}\left(W\right)\right)$$
7		sitgval.1	$$⊢\phi \to W\in V$$
8		sitgval.2	$$⊢\phi \to M\in \bigcup \mathrm{ran}\mathrm{measures}$$
9		sitg0.1	$$⊢\phi \to W\in \mathrm{TopSp}$$
10		sitg0.2	$$⊢\phi \to W\in \mathrm{Mnd}$$
11	1 2 3 4 5 6 7 8 9 10	sibf0	$$⊢\phi \to \bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\in {\Im }_M^W$$
12	1 2 3 4 5 6 7 8 11	sitgfval	$$⊢\phi \to {\int }_{\Im }^W\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)dM=\underset{x\in \mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}}{{\sum }_W}\left(H\left(M\left({\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)$$
13		rnxpss	$$⊢\mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\subseteq \left\{\underset{\dot{}}{0}\right\}$$
14		ssdif0	$$⊢\mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\subseteq \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}=\varnothing$$
15	13 14	mpbi	$$⊢\mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}=\varnothing$$
16		mpteq1	$$⊢\mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}=\varnothing \to \left(x\in \left(\mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼H\left(M\left({\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)=\left(x\in \varnothing ⟼H\left(M\left({\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)$$
17	15 16	ax-mp	$$⊢\left(x\in \left(\mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼H\left(M\left({\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)=\left(x\in \varnothing ⟼H\left(M\left({\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)$$
18		mpt0	$$⊢\left(x\in \varnothing ⟼H\left(M\left({\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)=\varnothing$$
19	17 18	eqtri	$$⊢\left(x\in \left(\mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼H\left(M\left({\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)=\varnothing$$
20	19	oveq2i	$$⊢\underset{x\in \mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}}{{\sum }_W}\left(H\left(M\left({\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)={\sum }_W\varnothing$$
21	4	gsum0	$$⊢{\sum }_W\varnothing =\underset{\dot{}}{0}$$
22	20 21	eqtri	$$⊢\underset{x\in \mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}}{{\sum }_W}\left(H\left(M\left({\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)=\underset{\dot{}}{0}$$
23	12 22	eqtrdi	$$⊢\phi \to {\int }_{\Im }^W\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)dM=\underset{\dot{}}{0}$$