Description: Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the complex 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 ) ) |
||
sitgclcn.1 | |- ( ph -> W e. Ban ) |
||
sitgclcn.2 | |- ( ph -> ( Scalar ` W ) = CCfld ) |
||
Assertion | sitgclcn | |- ( ph -> ( ( W sitg M ) ` F ) e. B ) |
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 | sitgclcn.1 | |- ( ph -> W e. Ban ) |
|
11 | sitgclcn.2 | |- ( ph -> ( Scalar ` W ) = CCfld ) |
|
12 | cnrrext | |- CCfld 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 ) |