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 | |
|
sitgval.j | |
||
sitgval.s | |
||
sitgval.0 | |
||
sitgval.x | |
||
sitgval.h | |
||
sitgval.1 | |
||
sitgval.2 | |
||
sibfmbl.1 | |
||
sitgclbn.1 | |
||
sitgclbn.2 | |
||
Assertion | sitgclbn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sitgval.b | |
|
2 | sitgval.j | |
|
3 | sitgval.s | |
|
4 | sitgval.0 | |
|
5 | sitgval.x | |
|
6 | sitgval.h | |
|
7 | sitgval.1 | |
|
8 | sitgval.2 | |
|
9 | sibfmbl.1 | |
|
10 | sitgclbn.1 | |
|
11 | sitgclbn.2 | |
|
12 | eqid | |
|
13 | eqid | |
|
14 | bncms | |
|
15 | 10 14 | syl | |
16 | cmsms | |
|
17 | mstps | |
|
18 | 15 16 17 | 3syl | |
19 | bnlmod | |
|
20 | lmodcmn | |
|
21 | 10 19 20 | 3syl | |
22 | 10 19 | syl | |
23 | 22 | 3ad2ant1 | |
24 | imassrn | |
|
25 | 6 | rneqi | |
26 | eqid | |
|
27 | 26 | rrhfe | |
28 | frn | |
|
29 | 11 27 28 | 3syl | |
30 | 25 29 | eqsstrid | |
31 | 24 30 | sstrid | |
32 | 31 | sselda | |
33 | 32 | 3adant3 | |
34 | simp3 | |
|
35 | 1 12 5 26 | lmodvscl | |
36 | 23 33 34 35 | syl3anc | |
37 | 1 2 3 4 5 6 7 8 9 12 13 18 21 11 36 | sitgclg | |