Metamath Proof Explorer

Theorem sitgval

Description: Value of the simple function integral builder for a given space W and measure M . (Contributed by Thierry Arnoux, 30-Jan-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
Assertion 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

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 7 elexd ⊢φ→W∈V
10 2fveq3 ⊢w=W→𝛔⁡TopOpen⁡w=𝛔⁡TopOpen⁡W
11 2 fveq2i ⊢𝛔⁡J=𝛔⁡TopOpen⁡W
12 3 11 eqtri ⊢S=𝛔⁡TopOpen⁡W
13 10 12 eqtr4di ⊢w=W→𝛔⁡TopOpen⁡w=S
14 13 oveq2d ⊢w=W→dom⁡mMblFnμ𝛔⁡TopOpen⁡w=dom⁡mMblFnμS
15 fveq2 ⊢w=W→0w=0W
16 15 4 eqtr4di ⊢w=W→0w=0˙
17 16 sneqd ⊢w=W→0w=0˙
18 17 difeq2d ⊢w=W→ran⁡g∖0w=ran⁡g∖0˙
19 18 raleqdv ⊢w=W→∀x∈ran⁡g∖0wm⁡g-1x∈0+∞↔∀x∈ran⁡g∖0˙m⁡g-1x∈0+∞
20 19 anbi2d ⊢w=W→ran⁡g∈Fin∧∀x∈ran⁡g∖0wm⁡g-1x∈0+∞↔ran⁡g∈Fin∧∀x∈ran⁡g∖0˙m⁡g-1x∈0+∞
21 14 20 rabeqbidv ⊢w=W→g∈dom⁡mMblFnμ𝛔⁡TopOpen⁡w|ran⁡g∈Fin∧∀x∈ran⁡g∖0wm⁡g-1x∈0+∞=g∈dom⁡mMblFnμS|ran⁡g∈Fin∧∀x∈ran⁡g∖0˙m⁡g-1x∈0+∞
22 id ⊢w=W→w=W
23 17 difeq2d ⊢w=W→ran⁡f∖0w=ran⁡f∖0˙
24 fveq2 ⊢w=W→⋅w=⋅W
25 24 5 eqtr4di ⊢w=W→⋅w=·˙
26 2fveq3 ⊢w=W→ℝHom⁡Scalar⁡w=ℝHom⁡Scalar⁡W
27 26 6 eqtr4di ⊢w=W→ℝHom⁡Scalar⁡w=H
28 27 fveq1d ⊢w=W→ℝHom⁡Scalar⁡w⁡m⁡f-1x=H⁡m⁡f-1x
29 eqidd ⊢w=W→x=x
30 25 28 29 oveq123d ⊢w=W→ℝHom⁡Scalar⁡w⁡m⁡f-1x⋅wx=H⁡m⁡f-1x·˙x
31 23 30 mpteq12dv ⊢w=W→x∈ran⁡f∖0w⟼ℝHom⁡Scalar⁡w⁡m⁡f-1x⋅wx=x∈ran⁡f∖0˙⟼H⁡m⁡f-1x·˙x
32 22 31 oveq12d ⊢w=W→∑wx∈ran⁡f∖0wℝHom⁡Scalar⁡w⁡m⁡f-1x⋅wx=∑Wx∈ran⁡f∖0˙H⁡m⁡f-1x·˙x
33 21 32 mpteq12dv ⊢w=W→f∈g∈dom⁡mMblFnμ𝛔⁡TopOpen⁡w|ran⁡g∈Fin∧∀x∈ran⁡g∖0wm⁡g-1x∈0+∞⟼∑wx∈ran⁡f∖0wℝHom⁡Scalar⁡w⁡m⁡f-1x⋅wx=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
34 dmeq ⊢m=M→dom⁡m=dom⁡M
35 34 oveq1d ⊢m=M→dom⁡mMblFnμS=dom⁡MMblFnμS
36 fveq1 ⊢m=M→m⁡g-1x=M⁡g-1x
37 36 eleq1d ⊢m=M→m⁡g-1x∈0+∞↔M⁡g-1x∈0+∞
38 37 ralbidv ⊢m=M→∀x∈ran⁡g∖0˙m⁡g-1x∈0+∞↔∀x∈ran⁡g∖0˙M⁡g-1x∈0+∞
39 38 anbi2d ⊢m=M→ran⁡g∈Fin∧∀x∈ran⁡g∖0˙m⁡g-1x∈0+∞↔ran⁡g∈Fin∧∀x∈ran⁡g∖0˙M⁡g-1x∈0+∞
40 35 39 rabeqbidv ⊢m=M→g∈dom⁡mMblFnμS|ran⁡g∈Fin∧∀x∈ran⁡g∖0˙m⁡g-1x∈0+∞=g∈dom⁡MMblFnμS|ran⁡g∈Fin∧∀x∈ran⁡g∖0˙M⁡g-1x∈0+∞
41 simpl ⊢m=M∧x∈ran⁡f∖0˙→m=M
42 41 fveq1d ⊢m=M∧x∈ran⁡f∖0˙→m⁡f-1x=M⁡f-1x
43 42 fveq2d ⊢m=M∧x∈ran⁡f∖0˙→H⁡m⁡f-1x=H⁡M⁡f-1x
44 43 oveq1d ⊢m=M∧x∈ran⁡f∖0˙→H⁡m⁡f-1x·˙x=H⁡M⁡f-1x·˙x
45 44 mpteq2dva ⊢m=M→x∈ran⁡f∖0˙⟼H⁡m⁡f-1x·˙x=x∈ran⁡f∖0˙⟼H⁡M⁡f-1x·˙x
46 45 oveq2d ⊢m=M→∑Wx∈ran⁡f∖0˙H⁡m⁡f-1x·˙x=∑Wx∈ran⁡f∖0˙H⁡M⁡f-1x·˙x
47 40 46 mpteq12dv ⊢m=M→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=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
48 df-sitg ⊢sitg=w∈V,m∈⋃ran⁡measures⟼f∈g∈dom⁡mMblFnμ𝛔⁡TopOpen⁡w|ran⁡g∈Fin∧∀x∈ran⁡g∖0wm⁡g-1x∈0+∞⟼∑wx∈ran⁡f∖0wℝHom⁡Scalar⁡w⁡m⁡f-1x⋅wx
49 ovex ⊢dom⁡MMblFnμS∈V
50 49 mptrabex ⊢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∈V
51 33 47 48 50 ovmpo ⊢W∈V∧M∈⋃ran⁡measures→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
52 9 8 51 syl2anc ⊢φ→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