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 = ( sigaGen ` J )
	sitgval.0	\|- .0. = ( 0g ` W )
	sitgval.x	\|- .x. = ( .s ` W )
	sitgval.h	\|- H = ( RRHom ` ( Scalar ` W ) )
	sitgval.1	\|- ( ph -> W e. V )
	sitgval.2	\|- ( ph -> M e. U. ran measures )
	sibfmbl.1	\|- ( ph -> F e. dom ( W sitg M ) )
	sitgclbn.1	\|- ( ph -> W e. Ban )
	sitgclbn.2	\|- ( ph -> ( Scalar ` W ) e. RRExt )
Assertion	sitgclbn	\|- ( ph -> ( ( W sitg M ) ` F ) e. B )

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	\|- B = ( Base ` W )
2		sitgval.j	\|- J = ( TopOpen ` W )
3		sitgval.s	\|- S = ( sigaGen ` J )
4		sitgval.0	\|- .0. = ( 0g ` W )
5		sitgval.x	\|- .x. = ( .s ` W )
6		sitgval.h	\|- H = ( RRHom ` ( Scalar ` W ) )
7		sitgval.1	\|- ( ph -> W e. V )
8		sitgval.2	\|- ( ph -> M e. U. ran measures )
9		sibfmbl.1	\|- ( ph -> F e. dom ( W sitg M ) )
10		sitgclbn.1	\|- ( ph -> W e. Ban )
11		sitgclbn.2	\|- ( ph -> ( Scalar ` W ) e. RRExt )
12		eqid	\|- ( Scalar ` W ) = ( Scalar ` W )
13		eqid	\|- ( ( dist ` ( Scalar ` W ) ) \|` ( ( Base ` ( Scalar ` W ) ) X. ( Base ` ( Scalar ` W ) ) ) ) = ( ( dist ` ( Scalar ` W ) ) \|` ( ( Base ` ( Scalar ` W ) ) X. ( Base ` ( Scalar ` W ) ) ) )
14		bncms	\|- ( W e. Ban -> W e. CMetSp )
15		cmsms	\|- ( W e. CMetSp -> W e. MetSp )
16		mstps	\|- ( W e. MetSp -> W e. TopSp )
17	10 14 15 16	4syl	\|- ( ph -> W e. TopSp )
18		bnlmod	\|- ( W e. Ban -> W e. LMod )
19		lmodcmn	\|- ( W e. LMod -> W e. CMnd )
20	10 18 19	3syl	\|- ( ph -> W e. CMnd )
21	10 18	syl	\|- ( ph -> W e. LMod )
22	21	3ad2ant1	\|- ( ( ph /\ m e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> W e. LMod )
23		imassrn	\|- ( H " ( 0 [,) +oo ) ) C_ ran H
24	6	rneqi	\|- ran H = ran ( RRHom ` ( Scalar ` W ) )
25		eqid	\|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
26	25	rrhfe	\|- ( ( Scalar ` W ) e. RRExt -> ( RRHom ` ( Scalar ` W ) ) : RR --> ( Base ` ( Scalar ` W ) ) )
27		frn	\|- ( ( RRHom ` ( Scalar ` W ) ) : RR --> ( Base ` ( Scalar ` W ) ) -> ran ( RRHom ` ( Scalar ` W ) ) C_ ( Base ` ( Scalar ` W ) ) )
28	11 26 27	3syl	\|- ( ph -> ran ( RRHom ` ( Scalar ` W ) ) C_ ( Base ` ( Scalar ` W ) ) )
29	24 28	eqsstrid	\|- ( ph -> ran H C_ ( Base ` ( Scalar ` W ) ) )
30	23 29	sstrid	\|- ( ph -> ( H " ( 0 [,) +oo ) ) C_ ( Base ` ( Scalar ` W ) ) )
31	30	sselda	\|- ( ( ph /\ m e. ( H " ( 0 [,) +oo ) ) ) -> m e. ( Base ` ( Scalar ` W ) ) )
32	31	3adant3	\|- ( ( ph /\ m e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> m e. ( Base ` ( Scalar ` W ) ) )
33		simp3	\|- ( ( ph /\ m e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> x e. B )
34	1 12 5 25	lmodvscl	\|- ( ( W e. LMod /\ m e. ( Base ` ( Scalar ` W ) ) /\ x e. B ) -> ( m .x. x ) e. B )
35	22 32 33 34	syl3anc	\|- ( ( ph /\ m e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> ( m .x. x ) e. B )
36	1 2 3 4 5 6 7 8 9 12 13 17 20 11 35	sitgclg	\|- ( ph -> ( ( W sitg M ) ` F ) e. B )

Metamath Proof Explorer

Theorem sitgclbn

Proof