Theorem 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	⊢ 𝐵 = ( Base ‘ 𝑊 )
	sitgval.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
	sitgval.s	⊢ 𝑆 = ( sigaGen ‘ 𝐽 )
	sitgval.0	⊢ 0 = ( 0g ‘ 𝑊 )
	sitgval.x	⊢ · = ( ·𝑠 ‘ 𝑊 )
	sitgval.h	⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
	sitgval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
	sitgval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
	sibfmbl.1	⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
	sitgclbn.1	⊢ ( 𝜑 → 𝑊 ∈ Ban )
	sitgclbn.2	⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ ℝExt )
Assertion	sitgclbn	⊢ ( 𝜑 → ( ( 𝑊 sitg 𝑀 ) ‘ 𝐹 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		sitgval.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3		sitgval.s	⊢ 𝑆 = ( sigaGen ‘ 𝐽 )
4		sitgval.0	⊢ 0 = ( 0g ‘ 𝑊 )
5		sitgval.x	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		sitgval.h	⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
7		sitgval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
8		sitgval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
9		sibfmbl.1	⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
10		sitgclbn.1	⊢ ( 𝜑 → 𝑊 ∈ Ban )
11		sitgclbn.2	⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ ℝExt )
12		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
13		eqid	⊢ ( ( dist ‘ ( Scalar ‘ 𝑊 ) ) ↾ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) × ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ) = ( ( dist ‘ ( Scalar ‘ 𝑊 ) ) ↾ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) × ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
14		bncms	⊢ ( 𝑊 ∈ Ban → 𝑊 ∈ CMetSp )
15		cmsms	⊢ ( 𝑊 ∈ CMetSp → 𝑊 ∈ MetSp )
16		mstps	⊢ ( 𝑊 ∈ MetSp → 𝑊 ∈ TopSp )
17	10 14 15 16	4syl	⊢ ( 𝜑 → 𝑊 ∈ TopSp )
18		bnlmod	⊢ ( 𝑊 ∈ Ban → 𝑊 ∈ LMod )
19		lmodcmn	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ CMnd )
20	10 18 19	3syl	⊢ ( 𝜑 → 𝑊 ∈ CMnd )
21	10 18	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
22	21	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑊 ∈ LMod )
23		imassrn	⊢ ( 𝐻 “ ( 0 [,) +∞ ) ) ⊆ ran 𝐻
24	6	rneqi	⊢ ran 𝐻 = ran ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
25		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
26	25	rrhfe	⊢ ( ( Scalar ‘ 𝑊 ) ∈ ℝExt → ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) : ℝ ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
27		frn	⊢ ( ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) : ℝ ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) → ran ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) ⊆ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
28	11 26 27	3syl	⊢ ( 𝜑 → ran ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) ⊆ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
29	24 28	eqsstrid	⊢ ( 𝜑 → ran 𝐻 ⊆ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
30	23 29	sstrid	⊢ ( 𝜑 → ( 𝐻 “ ( 0 [,) +∞ ) ) ⊆ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
31	30	sselda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ) → 𝑚 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
32	31	3adant3	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑚 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
33		simp3	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
34	1 12 5 25	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑚 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑚 · 𝑥 ) ∈ 𝐵 )
35	22 32 33 34	syl3anc	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑚 · 𝑥 ) ∈ 𝐵 )
36	1 2 3 4 5 6 7 8 9 12 13 17 20 11 35	sitgclg	⊢ ( 𝜑 → ( ( 𝑊 sitg 𝑀 ) ‘ 𝐹 ) ∈ 𝐵 )