Metamath Proof Explorer

Theorem sitgf

Description: The integral for simple functions is itself a function. (Contributed by Thierry Arnoux, 13-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
sitgf.1 ⊢ φ ∧ f ∈ ℑ M W → ∫ ℑ W f dM ∈ B
Assertion sitgf ⊢ φ → W sitg M : ℑ M W ⟶ 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 sitgf.1 ⊢ φ ∧ f ∈ ℑ M W → ∫ ℑ W f dM ∈ B
10 funmpt ⊢ Fun ⁡ f ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ⟼ ∑ W x ∈ ran ⁡ f ∖ 0 ˙ H ⁡ M ⁡ f -1 x · ˙ x
11 1 2 3 4 5 6 7 8 sitgval ⊢ φ → W sitg M = f ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ⟼ ∑ W x ∈ ran ⁡ f ∖ 0 ˙ H ⁡ M ⁡ f -1 x · ˙ x
12 11 funeqd ⊢ φ → Fun ⁡ W sitg M ↔ Fun ⁡ f ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ⟼ ∑ W x ∈ ran ⁡ f ∖ 0 ˙ H ⁡ M ⁡ f -1 x · ˙ x
13 10 12 mpbiri ⊢ φ → Fun ⁡ W sitg M
14 13 funfnd ⊢ φ → W sitg M Fn ℑ M W
15 9 ralrimiva ⊢ φ → ∀ f ∈ ℑ M W ∫ ℑ W f dM ∈ B
16 fnfvrnss ⊢ W sitg M Fn ℑ M W ∧ ∀ f ∈ ℑ M W ∫ ℑ W f dM ∈ B → ran ⁡ W sitg M ⊆ B
17 14 15 16 syl2anc ⊢ φ → ran ⁡ W sitg M ⊆ B
18 df-f ⊢ W sitg M : ℑ M W ⟶ B ↔ W sitg M Fn ℑ M W ∧ ran ⁡ W sitg M ⊆ B
19 14 17 18 sylanbrc ⊢ φ → W sitg M : ℑ M W ⟶ B