Theorem sibf0

Description: The constant zero function is a simple function. (Contributed by Thierry Arnoux, 4-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}$$
	sibf0.1	$$⊢\phi \to W\in \mathrm{TopSp}$$
	sibf0.2	$$⊢\phi \to W\in \mathrm{Mnd}$$
Assertion	sibf0	$$⊢\phi \to \bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\in {\Im }_M^W$$

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		sibf0.1	$$⊢\phi \to W\in \mathrm{TopSp}$$
10		sibf0.2	$$⊢\phi \to W\in \mathrm{Mnd}$$
11		dmmeas	$$⊢M\in \bigcup \mathrm{ran}\mathrm{measures}\to \mathrm{dom}M\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
12	8 11	syl	$$⊢\phi \to \mathrm{dom}M\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
13	2	fvexi	$$⊢J\in \mathrm{V}$$
14	13	a1i	$$⊢\phi \to J\in \mathrm{V}$$
15	14	sgsiga	$$⊢\phi \to 𝛔\left(J\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
16	3 15	eqeltrid	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
17		fconstmpt	$$⊢\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}=\left(x\in \bigcup \mathrm{dom}M⟼\underset{\dot{}}{0}\right)$$
18	17	a1i	$$⊢\phi \to \bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}=\left(x\in \bigcup \mathrm{dom}M⟼\underset{\dot{}}{0}\right)$$
19	1 4	mndidcl	$$⊢W\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in B$$
20	10 19	syl	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
21	1 2	tpsuni	$$⊢W\in \mathrm{TopSp}\to B=\bigcup J$$
22	9 21	syl	$$⊢\phi \to B=\bigcup J$$
23	3	unieqi	$$⊢\bigcup S=\bigcup 𝛔\left(J\right)$$
24		unisg	$$⊢J\in \mathrm{V}\to \bigcup 𝛔\left(J\right)=\bigcup J$$
25	13 24	mp1i	$$⊢\phi \to \bigcup 𝛔\left(J\right)=\bigcup J$$
26	23 25	syl5eq	$$⊢\phi \to \bigcup S=\bigcup J$$
27	22 26	eqtr4d	$$⊢\phi \to B=\bigcup S$$
28	20 27	eleqtrd	$$⊢\phi \to \underset{\dot{}}{0}\in \bigcup S$$
29	12 16 18 28	mbfmcst	$$⊢\phi \to \bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }S\right)$$
30		xpeq1	$$⊢\bigcup \mathrm{dom}M=\varnothing \to \bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}=\varnothing \times \left\{\underset{\dot{}}{0}\right\}$$
31		0xp	$$⊢\varnothing \times \left\{\underset{\dot{}}{0}\right\}=\varnothing$$
32	30 31	eqtrdi	$$⊢\bigcup \mathrm{dom}M=\varnothing \to \bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}=\varnothing$$
33	32	rneqd	$$⊢\bigcup \mathrm{dom}M=\varnothing \to \mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)=\mathrm{ran}\varnothing$$
34		rn0	$$⊢\mathrm{ran}\varnothing =\varnothing$$
35	33 34	eqtrdi	$$⊢\bigcup \mathrm{dom}M=\varnothing \to \mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)=\varnothing$$
36		0fin	$$⊢\varnothing \in \mathrm{Fin}$$
37	35 36	eqeltrdi	$$⊢\bigcup \mathrm{dom}M=\varnothing \to \mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Fin}$$
38		rnxp	$$⊢\bigcup \mathrm{dom}M\ne \varnothing \to \mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
39		snfi	$$⊢\left\{\underset{\dot{}}{0}\right\}\in \mathrm{Fin}$$
40	38 39	eqeltrdi	$$⊢\bigcup \mathrm{dom}M\ne \varnothing \to \mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Fin}$$
41	37 40	pm2.61ine	$$⊢\mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Fin}$$
42	41	a1i	$$⊢\phi \to \mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Fin}$$
43		noel	$$⊢\neg x\in \varnothing$$
44	35	difeq1d	$$⊢\bigcup \mathrm{dom}M=\varnothing \to \mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}=\varnothing \setminus \left\{\underset{\dot{}}{0}\right\}$$
45		0dif	$$⊢\varnothing \setminus \left\{\underset{\dot{}}{0}\right\}=\varnothing$$
46	44 45	eqtrdi	$$⊢\bigcup \mathrm{dom}M=\varnothing \to \mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}=\varnothing$$
47	38	difeq1d	$$⊢\bigcup \mathrm{dom}M\ne \varnothing \to \mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}=\left\{\underset{\dot{}}{0}\right\}\setminus \left\{\underset{\dot{}}{0}\right\}$$
48		difid	$$⊢\left\{\underset{\dot{}}{0}\right\}\setminus \left\{\underset{\dot{}}{0}\right\}=\varnothing$$
49	47 48	eqtrdi	$$⊢\bigcup \mathrm{dom}M\ne \varnothing \to \mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}=\varnothing$$
50	46 49	pm2.61ine	$$⊢\mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}=\varnothing$$
51	50	eleq2i	$$⊢x\in \left(\mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow x\in \varnothing$$
52	43 51	mtbir	$$⊢\neg x\in \left(\mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
53	52	pm2.21i	$$⊢x\in \left(\mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to M\left({\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)$$
54	53	adantl	$$⊢\left(\phi \wedge x\in \left(\mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to M\left({\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)$$
55	54	ralrimiva	$$⊢\phi \to \forall x\in \left(\mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left({\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)$$
56	1 2 3 4 5 6 7 8	issibf	$$⊢\phi \to \left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\in {\Im }_M^W\leftrightarrow \left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }S\right)\wedge \mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Fin}\wedge \forall x\in \left(\mathrm{ran}\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left({\left(\bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\right)}^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)$$
57	29 42 55 56	mpbir3and	$$⊢\phi \to \bigcup \mathrm{dom}M\times \left\{\underset{\dot{}}{0}\right\}\in {\Im }_M^W$$