Theorem sitgclre

Description: Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the real numbers. (Contributed by Thierry Arnoux, 24-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$$
	sitgclre.1	$$⊢\phi \to W\in \mathrm{Ban}$$
	sitgclre.3	$$⊢\phi \to \mathrm{Scalar}\left(W\right)={ℝ}_{\mathrm{fld}}$$
Assertion	sitgclre	$$⊢\phi \to {\int }_{\Im }^{W}FdM\in B$$

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		sitgclre.1	$$⊢\phi \to W\in \mathrm{Ban}$$
11		sitgclre.3	$$⊢\phi \to \mathrm{Scalar}\left(W\right)={ℝ}_{\mathrm{fld}}$$
12		rerrext	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{ℝExt}$$
13	11 12	eqeltrdi	$$⊢\phi \to \mathrm{Scalar}\left(W\right)\in \mathrm{ℝExt}$$
14	1 2 3 4 5 6 7 8 9 10 13	sitgclbn	$$⊢\phi \to {\int }_{\Im }^{W}FdM\in B$$