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	10 14	syl	⊢ ( 𝜑 → 𝑊 ∈ CMetSp )
16		cmsms	⊢ ( 𝑊 ∈ CMetSp → 𝑊 ∈ MetSp )
17		mstps	⊢ ( 𝑊 ∈ MetSp → 𝑊 ∈ TopSp )
18	15 16 17	3syl	⊢ ( 𝜑 → 𝑊 ∈ TopSp )
19		bnlmod	⊢ ( 𝑊 ∈ Ban → 𝑊 ∈ LMod )
20		lmodcmn	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ CMnd )
21	10 19 20	3syl	⊢ ( 𝜑 → 𝑊 ∈ CMnd )
22	10 19	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
23	22	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑊 ∈ LMod )
24		imassrn	⊢ ( 𝐻 “ ( 0 [,) +∞ ) ) ⊆ ran 𝐻
25	6	rneqi	⊢ ran 𝐻 = ran ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
26		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
27	26	rrhfe	⊢ ( ( Scalar ‘ 𝑊 ) ∈ ℝExt → ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) : ℝ ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
28		frn	⊢ ( ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) : ℝ ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) → ran ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) ⊆ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
29	11 27 28	3syl	⊢ ( 𝜑 → ran ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) ⊆ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
30	25 29	eqsstrid	⊢ ( 𝜑 → ran 𝐻 ⊆ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
31	24 30	sstrid	⊢ ( 𝜑 → ( 𝐻 “ ( 0 [,) +∞ ) ) ⊆ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
32	31	sselda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ) → 𝑚 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
33	32	3adant3	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑚 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
34		simp3	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
35	1 12 5 26	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑚 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑚 · 𝑥 ) ∈ 𝐵 )
36	23 33 34 35	syl3anc	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑚 · 𝑥 ) ∈ 𝐵 )
37	1 2 3 4 5 6 7 8 9 12 13 18 21 11 36	sitgclg	⊢ ( 𝜑 → ( ( 𝑊 sitg 𝑀 ) ‘ 𝐹 ) ∈ 𝐵 )