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 𝐵 = ( Base ‘ 𝑊 )
sitgval.j 𝐽 = ( TopOpen ‘ 𝑊 )
sitgval.s 𝑆 = ( sigaGen ‘ 𝐽 )
sitgval.0 0 = ( 0g𝑊 )
sitgval.x · = ( ·𝑠𝑊 )
sitgval.h 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
sitgval.1 ( 𝜑𝑊𝑉 )
sitgval.2 ( 𝜑𝑀 ran measures )
Assertion sitgval ( 𝜑 → ( 𝑊 sitg 𝑀 ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) )

Proof

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 7 elexd ( 𝜑𝑊 ∈ V )
10 2fveq3 ( 𝑤 = 𝑊 → ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) = ( sigaGen ‘ ( TopOpen ‘ 𝑊 ) ) )
11 2 fveq2i ( sigaGen ‘ 𝐽 ) = ( sigaGen ‘ ( TopOpen ‘ 𝑊 ) )
12 3 11 eqtri 𝑆 = ( sigaGen ‘ ( TopOpen ‘ 𝑊 ) )
13 10 12 eqtr4di ( 𝑤 = 𝑊 → ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) = 𝑆 )
14 13 oveq2d ( 𝑤 = 𝑊 → ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) = ( dom 𝑚 MblFnM 𝑆 ) )
15 fveq2 ( 𝑤 = 𝑊 → ( 0g𝑤 ) = ( 0g𝑊 ) )
16 15 4 eqtr4di ( 𝑤 = 𝑊 → ( 0g𝑤 ) = 0 )
17 16 sneqd ( 𝑤 = 𝑊 → { ( 0g𝑤 ) } = { 0 } )
18 17 difeq2d ( 𝑤 = 𝑊 → ( ran 𝑔 ∖ { ( 0g𝑤 ) } ) = ( ran 𝑔 ∖ { 0 } ) )
19 18 raleqdv ( 𝑤 = 𝑊 → ( ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g𝑤 ) } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ↔ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) )
20 19 anbi2d ( 𝑤 = 𝑊 → ( ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g𝑤 ) } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ↔ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) )
21 14 20 rabeqbidv ( 𝑤 = 𝑊 → { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g𝑤 ) } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } = { 𝑔 ∈ ( dom 𝑚 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } )
22 id ( 𝑤 = 𝑊𝑤 = 𝑊 )
23 17 difeq2d ( 𝑤 = 𝑊 → ( ran 𝑓 ∖ { ( 0g𝑤 ) } ) = ( ran 𝑓 ∖ { 0 } ) )
24 fveq2 ( 𝑤 = 𝑊 → ( ·𝑠𝑤 ) = ( ·𝑠𝑊 ) )
25 24 5 eqtr4di ( 𝑤 = 𝑊 → ( ·𝑠𝑤 ) = · )
26 2fveq3 ( 𝑤 = 𝑊 → ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) )
27 26 6 eqtr4di ( 𝑤 = 𝑊 → ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) = 𝐻 )
28 27 fveq1d ( 𝑤 = 𝑊 → ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) = ( 𝐻 ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) )
29 eqidd ( 𝑤 = 𝑊𝑥 = 𝑥 )
30 25 28 29 oveq123d ( 𝑤 = 𝑊 → ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠𝑤 ) 𝑥 ) = ( ( 𝐻 ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) )
31 23 30 mpteq12dv ( 𝑤 = 𝑊 → ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠𝑤 ) 𝑥 ) ) = ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) )
32 22 31 oveq12d ( 𝑤 = 𝑊 → ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠𝑤 ) 𝑥 ) ) ) = ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) )
33 21 32 mpteq12dv ( 𝑤 = 𝑊 → ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g𝑤 ) } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠𝑤 ) 𝑥 ) ) ) ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) )
34 dmeq ( 𝑚 = 𝑀 → dom 𝑚 = dom 𝑀 )
35 34 oveq1d ( 𝑚 = 𝑀 → ( dom 𝑚 MblFnM 𝑆 ) = ( dom 𝑀 MblFnM 𝑆 ) )
36 fveq1 ( 𝑚 = 𝑀 → ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) = ( 𝑀 ‘ ( 𝑔 “ { 𝑥 } ) ) )
37 36 eleq1d ( 𝑚 = 𝑀 → ( ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ↔ ( 𝑀 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) )
38 37 ralbidv ( 𝑚 = 𝑀 → ( ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ↔ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) )
39 38 anbi2d ( 𝑚 = 𝑀 → ( ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ↔ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) )
40 35 39 rabeqbidv ( 𝑚 = 𝑀 → { 𝑔 ∈ ( dom 𝑚 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } = { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } )
41 simpl ( ( 𝑚 = 𝑀𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ) → 𝑚 = 𝑀 )
42 41 fveq1d ( ( 𝑚 = 𝑀𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ) → ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) = ( 𝑀 ‘ ( 𝑓 “ { 𝑥 } ) ) )
43 42 fveq2d ( ( 𝑚 = 𝑀𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ) → ( 𝐻 ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) = ( 𝐻 ‘ ( 𝑀 ‘ ( 𝑓 “ { 𝑥 } ) ) ) )
44 43 oveq1d ( ( 𝑚 = 𝑀𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ) → ( ( 𝐻 ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) = ( ( 𝐻 ‘ ( 𝑀 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) )
45 44 mpteq2dva ( 𝑚 = 𝑀 → ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) = ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) )
46 45 oveq2d ( 𝑚 = 𝑀 → ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) = ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) )
47 40 46 mpteq12dv ( 𝑚 = 𝑀 → ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) )
48 df-sitg sitg = ( 𝑤 ∈ V , 𝑚 ran measures ↦ ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g𝑤 ) } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠𝑤 ) 𝑥 ) ) ) ) )
49 ovex ( dom 𝑀 MblFnM 𝑆 ) ∈ V
50 49 mptrabex ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) ∈ V
51 33 47 48 50 ovmpo ( ( 𝑊 ∈ V ∧ 𝑀 ran measures ) → ( 𝑊 sitg 𝑀 ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) )
52 9 8 51 syl2anc ( 𝜑 → ( 𝑊 sitg 𝑀 ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) )