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	10 14	syl	$⊢ φ \to W \in CMetSp$
16		cmsms	$⊢ W \in CMetSp \to W \in MetSp$
17		mstps	$⊢ W \in MetSp \to W \in TopSp$
18	15 16 17	3syl	$⊢ φ \to W \in TopSp$
19		bnlmod	$⊢ W \in Ban \to W \in LMod$
20		lmodcmn	$⊢ W \in LMod \to W \in CMnd$
21	10 19 20	3syl	$⊢ φ \to W \in CMnd$
22	10 19	syl	$⊢ φ \to W \in LMod$
23	22	3ad2ant1	$⊢ (φ \land m \in H [[0, +∞)] \land x \in B) \to W \in LMod$
24		imassrn	$⊢ H [[0, +∞)] \subseteq ran H$
25	6	rneqi	$⊢ ran H = ran ℝHom (Scalar (W))$
26		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
27	26	rrhfe	$⊢ Scalar (W) \in ℝExt \to ℝHom (Scalar (W)) : ℝ ⟶ {Base}_{Scalar (W)}$
28		frn	$⊢ ℝHom (Scalar (W)) : ℝ ⟶ {Base}_{Scalar (W)} \to ran ℝHom (Scalar (W)) \subseteq {Base}_{Scalar (W)}$
29	11 27 28	3syl	$⊢ φ \to ran ℝHom (Scalar (W)) \subseteq {Base}_{Scalar (W)}$
30	25 29	eqsstrid	$⊢ φ \to ran H \subseteq {Base}_{Scalar (W)}$
31	24 30	sstrid	$⊢ φ \to H [[0, +∞)] \subseteq {Base}_{Scalar (W)}$
32	31	sselda	$⊢ (φ \land m \in H [[0, +∞)]) \to m \in {Base}_{Scalar (W)}$
33	32	3adant3	$⊢ (φ \land m \in H [[0, +∞)] \land x \in B) \to m \in {Base}_{Scalar (W)}$
34		simp3	$⊢ (φ \land m \in H [[0, +∞)] \land x \in B) \to x \in B$
35	1 12 5 26	lmodvscl	$⊢ (W \in LMod \land m \in {Base}_{Scalar (W)} \land x \in B) \to m \underset{˙}{\cdot} x \in B$
36	23 33 34 35	syl3anc	$⊢ (φ \land m \in H [[0, +∞)] \land x \in B) \to m \underset{˙}{\cdot} x \in B$
37	1 2 3 4 5 6 7 8 9 12 13 18 21 11 36	sitgclg	$⊢ φ \to \int_{ℑ}^{W} F d M \in B$

Metamath Proof Explorer

Theorem sitgclbn

Proof