Metamath Proof Explorer


Theorem 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=BaseW
sitgval.j J=TopOpenW
sitgval.s S=𝛔J
sitgval.0 0˙=0W
sitgval.x ·˙=W
sitgval.h H=ℝHomScalarW
sitgval.1 φWV
sitgval.2 φMranmeasures
sibfmbl.1 φFMW
sitgclbn.1 φWBan
sitgclbn.2 φScalarWℝExt
Assertion sitgclbn φWFdMB

Proof

Step Hyp Ref Expression
1 sitgval.b B=BaseW
2 sitgval.j J=TopOpenW
3 sitgval.s S=𝛔J
4 sitgval.0 0˙=0W
5 sitgval.x ·˙=W
6 sitgval.h H=ℝHomScalarW
7 sitgval.1 φWV
8 sitgval.2 φMranmeasures
9 sibfmbl.1 φFMW
10 sitgclbn.1 φWBan
11 sitgclbn.2 φScalarWℝExt
12 eqid ScalarW=ScalarW
13 eqid distScalarWBaseScalarW×BaseScalarW=distScalarWBaseScalarW×BaseScalarW
14 bncms WBanWCMetSp
15 10 14 syl φWCMetSp
16 cmsms WCMetSpWMetSp
17 mstps WMetSpWTopSp
18 15 16 17 3syl φWTopSp
19 bnlmod WBanWLMod
20 lmodcmn WLModWCMnd
21 10 19 20 3syl φWCMnd
22 10 19 syl φWLMod
23 22 3ad2ant1 φmH0+∞xBWLMod
24 imassrn H0+∞ranH
25 6 rneqi ranH=ranℝHomScalarW
26 eqid BaseScalarW=BaseScalarW
27 26 rrhfe ScalarWℝExtℝHomScalarW:BaseScalarW
28 frn ℝHomScalarW:BaseScalarWranℝHomScalarWBaseScalarW
29 11 27 28 3syl φranℝHomScalarWBaseScalarW
30 25 29 eqsstrid φranHBaseScalarW
31 24 30 sstrid φH0+∞BaseScalarW
32 31 sselda φmH0+∞mBaseScalarW
33 32 3adant3 φmH0+∞xBmBaseScalarW
34 simp3 φmH0+∞xBxB
35 1 12 5 26 lmodvscl WLModmBaseScalarWxBm·˙xB
36 23 33 34 35 syl3anc φmH0+∞xBm·˙xB
37 1 2 3 4 5 6 7 8 9 12 13 18 21 11 36 sitgclg φWFdMB