Theorem sitgclre

Description: Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the real numbers. (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 ) )
	sitgclre.1	|- ( ph -> W e. Ban )
	sitgclre.3	|- ( ph -> ( Scalar ` W ) = RRfld )
Assertion	sitgclre	|- ( 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		sitgclre.1	|- ( ph -> W e. Ban )
11		sitgclre.3	|- ( ph -> ( Scalar ` W ) = RRfld )
12		rerrext	|- RRfld e. RRExt
13	11 12	eqeltrdi	|- ( ph -> ( Scalar ` W ) e. RRExt )
14	1 2 3 4 5 6 7 8 9 10 13	sitgclbn	|- ( ph -> ( ( W sitg M ) ` F ) e. B )