Theorem sibfima

Description: Any preimage of a singleton by a simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-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}$$
	sibfmbl.1	$$⊢\phi \to F\in {\Im }_M^W$$
Assertion	sibfima	$$⊢\left(\phi \wedge A\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to M\left(F^{-1}\left[\left\{A\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)$$

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		sibfmbl.1	$$⊢\phi \to F\in {\Im }_M^W$$
10	1 2 3 4 5 6 7 8	issibf	$$⊢\phi \to \left(F\in {\Im }_M^W\leftrightarrow \left(F\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }S\right)\wedge \mathrm{ran}F\in \mathrm{Fin}\wedge \forall x\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(F^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)$$
11	9 10	mpbid	$$⊢\phi \to \left(F\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }S\right)\wedge \mathrm{ran}F\in \mathrm{Fin}\wedge \forall x\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(F^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)$$
12	11	simp3d	$$⊢\phi \to \forall x\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(F^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)$$
13		sneq	$$⊢x=A\to \left\{x\right\}=\left\{A\right\}$$
14	13	imaeq2d	$$⊢x=A\to F^{-1}\left[\left\{x\right\}\right]=F^{-1}\left[\left\{A\right\}\right]$$
15	14	fveq2d	$$⊢x=A\to M\left(F^{-1}\left[\left\{x\right\}\right]\right)=M\left(F^{-1}\left[\left\{A\right\}\right]\right)$$
16	15	eleq1d	$$⊢x=A\to \left(M\left(F^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\leftrightarrow M\left(F^{-1}\left[\left\{A\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)$$
17	16	rspcv	$$⊢A\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to \left(\forall x\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(F^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\to M\left(F^{-1}\left[\left\{A\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)$$
18	12 17	mpan9	$$⊢\left(\phi \wedge A\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to M\left(F^{-1}\left[\left\{A\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)$$