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 | ⊢ 𝐵 = ( Base ‘ 𝑊 ) | |
| sitgval.j | ⊢ 𝐽 = ( TopOpen ‘ 𝑊 ) | ||
| sitgval.s | ⊢ 𝑆 = ( sigaGen ‘ 𝐽 ) | ||
| sitgval.0 | ⊢ 0 = ( 0g ‘ 𝑊 ) | ||
| sitgval.x | ⊢ · = ( ·𝑠 ‘ 𝑊 ) | ||
| sitgval.h | ⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) | ||
| sitgval.1 | ⊢ ( 𝜑 → 𝑊 ∈ 𝑉 ) | ||
| sitgval.2 | ⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures ) | ||
| sibfmbl.1 | ⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) ) | ||
| sitgclre.1 | ⊢ ( 𝜑 → 𝑊 ∈ Ban ) | ||
| sitgclre.3 | ⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) = ℝfld ) | ||
| Assertion | sitgclre | ⊢ ( 𝜑 → ( ( 𝑊 sitg 𝑀 ) ‘ 𝐹 ) ∈ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sitgval.b | ⊢ 𝐵 = ( Base ‘ 𝑊 ) | |
| 2 | sitgval.j | ⊢ 𝐽 = ( TopOpen ‘ 𝑊 ) | |
| 3 | sitgval.s | ⊢ 𝑆 = ( sigaGen ‘ 𝐽 ) | |
| 4 | sitgval.0 | ⊢ 0 = ( 0g ‘ 𝑊 ) | |
| 5 | sitgval.x | ⊢ · = ( ·𝑠 ‘ 𝑊 ) | |
| 6 | sitgval.h | ⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) | |
| 7 | sitgval.1 | ⊢ ( 𝜑 → 𝑊 ∈ 𝑉 ) | |
| 8 | sitgval.2 | ⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures ) | |
| 9 | sibfmbl.1 | ⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) ) | |
| 10 | sitgclre.1 | ⊢ ( 𝜑 → 𝑊 ∈ Ban ) | |
| 11 | sitgclre.3 | ⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) = ℝfld ) | |
| 12 | rerrext | ⊢ ℝfld ∈ ℝExt | |
| 13 | 11 12 | eqeltrdi | ⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ ℝExt ) |
| 14 | 1 2 3 4 5 6 7 8 9 10 13 | sitgclbn | ⊢ ( 𝜑 → ( ( 𝑊 sitg 𝑀 ) ‘ 𝐹 ) ∈ 𝐵 ) |