Metamath Proof Explorer


Theorem sitgclcn

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 = 𝛔 J
sitgval.0 0 ˙ = 0 W
sitgval.x · ˙ = W
sitgval.h H = ℝHom Scalar W
sitgval.1 φ W V
sitgval.2 φ M ran measures
sibfmbl.1 φ F M W
sitgclcn.1 φ W Ban
sitgclcn.2 φ Scalar W = fld
Assertion sitgclcn φ W F dM B

Proof

Step Hyp Ref Expression
1 sitgval.b B = Base W
2 sitgval.j J = TopOpen W
3 sitgval.s S = 𝛔 J
4 sitgval.0 0 ˙ = 0 W
5 sitgval.x · ˙ = W
6 sitgval.h H = ℝHom Scalar W
7 sitgval.1 φ W V
8 sitgval.2 φ M ran measures
9 sibfmbl.1 φ F M W
10 sitgclcn.1 φ W Ban
11 sitgclcn.2 φ Scalar W = fld
12 cnrrext fld ℝExt
13 11 12 eqeltrdi φ Scalar W ℝExt
14 1 2 3 4 5 6 7 8 9 10 13 sitgclbn φ W F dM B