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	10 14	syl	\|- ( ph -> W e. CMetSp )
16		cmsms	\|- ( W e. CMetSp -> W e. MetSp )
17		mstps	\|- ( W e. MetSp -> W e. TopSp )
18	15 16 17	3syl	\|- ( ph -> W e. TopSp )
19		bnlmod	\|- ( W e. Ban -> W e. LMod )
20		lmodcmn	\|- ( W e. LMod -> W e. CMnd )
21	10 19 20	3syl	\|- ( ph -> W e. CMnd )
22	10 19	syl	\|- ( ph -> W e. LMod )
23	22	3ad2ant1	\|- ( ( ph /\ m e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> W e. LMod )
24		imassrn	\|- ( H " ( 0 [,) +oo ) ) C_ ran H
25	6	rneqi	\|- ran H = ran ( RRHom ` ( Scalar ` W ) )
26		eqid	\|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
27	26	rrhfe	\|- ( ( Scalar ` W ) e. RRExt -> ( RRHom ` ( Scalar ` W ) ) : RR --> ( Base ` ( Scalar ` W ) ) )
28		frn	\|- ( ( RRHom ` ( Scalar ` W ) ) : RR --> ( Base ` ( Scalar ` W ) ) -> ran ( RRHom ` ( Scalar ` W ) ) C_ ( Base ` ( Scalar ` W ) ) )
29	11 27 28	3syl	\|- ( ph -> ran ( RRHom ` ( Scalar ` W ) ) C_ ( Base ` ( Scalar ` W ) ) )
30	25 29	eqsstrid	\|- ( ph -> ran H C_ ( Base ` ( Scalar ` W ) ) )
31	24 30	sstrid	\|- ( ph -> ( H " ( 0 [,) +oo ) ) C_ ( Base ` ( Scalar ` W ) ) )
32	31	sselda	\|- ( ( ph /\ m e. ( H " ( 0 [,) +oo ) ) ) -> m e. ( Base ` ( Scalar ` W ) ) )
33	32	3adant3	\|- ( ( ph /\ m e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> m e. ( Base ` ( Scalar ` W ) ) )
34		simp3	\|- ( ( ph /\ m e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> x e. B )
35	1 12 5 26	lmodvscl	\|- ( ( W e. LMod /\ m e. ( Base ` ( Scalar ` W ) ) /\ x e. B ) -> ( m .x. x ) e. B )
36	23 33 34 35	syl3anc	\|- ( ( ph /\ m e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> ( m .x. x ) e. B )
37	1 2 3 4 5 6 7 8 9 12 13 18 21 11 36	sitgclg	\|- ( ph -> ( ( W sitg M ) ` F ) e. B )

Metamath Proof Explorer

Theorem sitgclbn

Proof