sitgclbn

Description: Closure of the Bochner integral on a simple function. This version is specific to Banach spaces, with additional conditions on its scalar field. (Contributed by Thierry Arnoux, 24-Feb-2018)

	Ref	Expression
Hypotheses	sitgval.b	$⊢ B = {Base}_{W}$
	sitgval.j	$⊢ J = TopOpen (W)$
	sitgval.s	$⊢ S = 𝛔 (J)$
	sitgval.0	$⊢ \underset{˙}{0} = 0_{W}$
	sitgval.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	sitgval.h	$⊢ H = ℝHom (Scalar (W))$
	sitgval.1	$⊢ φ \to W \in V$
	sitgval.2	$⊢ φ \to M \in ⋃ ran measures$
	sibfmbl.1	$⊢ φ \to F \in ℑ_{M}^{W}$
	sitgclbn.1	$⊢ φ \to W \in Ban$
	sitgclbn.2	$⊢ φ \to Scalar (W) \in ℝExt$
Assertion	sitgclbn	$⊢ φ \to \int_{ℑ}^{W} F d M \in B$

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	$⊢ B = {Base}_{W}$
2		sitgval.j	$⊢ J = TopOpen (W)$
3		sitgval.s	$⊢ S = 𝛔 (J)$
4		sitgval.0	$⊢ \underset{˙}{0} = 0_{W}$
5		sitgval.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		sitgval.h	$⊢ H = ℝHom (Scalar (W))$
7		sitgval.1	$⊢ φ \to W \in V$
8		sitgval.2	$⊢ φ \to M \in ⋃ ran measures$
9		sibfmbl.1	$⊢ φ \to F \in ℑ_{M}^{W}$
10		sitgclbn.1	$⊢ φ \to W \in Ban$
11		sitgclbn.2	$⊢ φ \to Scalar (W) \in ℝExt$
12		eqid	$⊢ Scalar (W) = Scalar (W)$
13		eqid	$⊢ {dist (Scalar (W)) ↾}_{({Base}_{Scalar (W)} \times {Base}_{Scalar (W)})} = {dist (Scalar (W)) ↾}_{({Base}_{Scalar (W)} \times {Base}_{Scalar (W)})}$
14		bncms	$⊢ W \in Ban \to W \in CMetSp$
15		cmsms	$⊢ W \in CMetSp \to W \in MetSp$
16		mstps	$⊢ W \in MetSp \to W \in TopSp$
17	10 14 15 16	4syl	$⊢ φ \to W \in TopSp$
18		bnlmod	$⊢ W \in Ban \to W \in LMod$
19		lmodcmn	$⊢ W \in LMod \to W \in CMnd$
20	10 18 19	3syl	$⊢ φ \to W \in CMnd$
21	10 18	syl	$⊢ φ \to W \in LMod$
22	21	3ad2ant1	$⊢ (φ \land m \in H [[0, +∞)] \land x \in B) \to W \in LMod$
23		imassrn	$⊢ H [[0, +∞)] \subseteq ran H$
24	6	rneqi	$⊢ ran H = ran ℝHom (Scalar (W))$
25		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
26	25	rrhfe	$⊢ Scalar (W) \in ℝExt \to ℝHom (Scalar (W)) : ℝ ⟶ {Base}_{Scalar (W)}$
27		frn	$⊢ ℝHom (Scalar (W)) : ℝ ⟶ {Base}_{Scalar (W)} \to ran ℝHom (Scalar (W)) \subseteq {Base}_{Scalar (W)}$
28	11 26 27	3syl	$⊢ φ \to ran ℝHom (Scalar (W)) \subseteq {Base}_{Scalar (W)}$
29	24 28	eqsstrid	$⊢ φ \to ran H \subseteq {Base}_{Scalar (W)}$
30	23 29	sstrid	$⊢ φ \to H [[0, +∞)] \subseteq {Base}_{Scalar (W)}$
31	30	sselda	$⊢ (φ \land m \in H [[0, +∞)]) \to m \in {Base}_{Scalar (W)}$
32	31	3adant3	$⊢ (φ \land m \in H [[0, +∞)] \land x \in B) \to m \in {Base}_{Scalar (W)}$
33		simp3	$⊢ (φ \land m \in H [[0, +∞)] \land x \in B) \to x \in B$
34	1 12 5 25	lmodvscl	$⊢ (W \in LMod \land m \in {Base}_{Scalar (W)} \land x \in B) \to m \underset{˙}{\cdot} x \in B$
35	22 32 33 34	syl3anc	$⊢ (φ \land m \in H [[0, +∞)] \land x \in B) \to m \underset{˙}{\cdot} x \in B$
36	1 2 3 4 5 6 7 8 9 12 13 17 20 11 35	sitgclg	$⊢ φ \to \int_{ℑ}^{W} F d M \in B$

Metamath Proof Explorer

Theorem sitgclbn

Proof