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=BaseW
sitgval.j ⊢J=TopOpen⁡W
sitgval.s ⊢S=𝛔⁡J
sitgval.0 ⊢0˙=0W
sitgval.x ⊢·˙=⋅W
sitgval.h ⊢H=ℝHom⁡Scalar⁡W
sitgval.1 ⊢φ→W∈V
sitgval.2 ⊢φ→M∈⋃ran⁡measures
sitgf.1 ⊢φ∧f∈ℑMW→∫ℑWfdM∈B
Assertion sitgf ⊢φ→WsitgM:ℑMW⟶B

Proof

Step Hyp Ref Expression
1 sitgval.b ⊢B=BaseW
2 sitgval.j ⊢J=TopOpen⁡W
3 sitgval.s ⊢S=𝛔⁡J
4 sitgval.0 ⊢0˙=0W
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∈ℑMW→∫ℑWfdM∈B
10 funmpt ⊢Fun⁡f∈g∈dom⁡MMblFnμS|ran⁡g∈Fin∧∀x∈ran⁡g∖0˙M⁡g-1x∈0+∞⟼∑Wx∈ran⁡f∖0˙H⁡M⁡f-1x·˙x
11 1 2 3 4 5 6 7 8 sitgval ⊢φ→WsitgM=f∈g∈dom⁡MMblFnμS|ran⁡g∈Fin∧∀x∈ran⁡g∖0˙M⁡g-1x∈0+∞⟼∑Wx∈ran⁡f∖0˙H⁡M⁡f-1x·˙x
12 11 funeqd ⊢φ→Fun⁡WsitgM↔Fun⁡f∈g∈dom⁡MMblFnμS|ran⁡g∈Fin∧∀x∈ran⁡g∖0˙M⁡g-1x∈0+∞⟼∑Wx∈ran⁡f∖0˙H⁡M⁡f-1x·˙x
13 10 12 mpbiri ⊢φ→Fun⁡WsitgM
14 13 funfnd ⊢φ→WsitgMFnℑMW
15 9 ralrimiva ⊢φ→∀f∈ℑMW∫ℑWfdM∈B
16 fnfvrnss ⊢WsitgMFnℑMW∧∀f∈ℑMW∫ℑWfdM∈B→ran⁡WsitgM⊆B
17 14 15 16 syl2anc ⊢φ→ran⁡WsitgM⊆B
18 df-f ⊢WsitgM:ℑMW⟶B↔WsitgMFnℑMW∧ran⁡WsitgM⊆B
19 14 17 18 sylanbrc ⊢φ→WsitgM:ℑMW⟶B