Metamath Proof Explorer

Theorem sitgfval

Description: Value of the Bochner integral for a simple function F . (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 )
sibfmbl.1 ⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
Assertion sitgfval ( 𝜑 → ( ( 𝑊 sitg 𝑀 ) ‘ 𝐹 ) = ( 𝑊 Σ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 sibfmbl.1 ⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
10 1 2 3 4 5 6 7 8 sitgval ⊢ ( 𝜑 → ( 𝑊 sitg 𝑀 ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
12 11 rneqd ⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ran 𝑓 = ran 𝐹 )
13 12 difeq1d ⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ( ran 𝑓 ∖ { 0 } ) = ( ran 𝐹 ∖ { 0 } ) )
14 11 cnveqd ⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ◡ 𝑓 = ◡ 𝐹 )
15 14 imaeq1d ⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ( ◡ 𝑓 “ { 𝑥 } ) = ( ◡ 𝐹 “ { 𝑥 } ) )
16 15 fveq2d ⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ( 𝑀 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) = ( 𝑀 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) )
17 16 fveq2d ⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) = ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) )
18 17 oveq1d ⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) = ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) )
19 13 18 mpteq12dv ⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) = ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) )
20 19 oveq2d ⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) = ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) )
21 1 2 3 4 5 6 7 8 9 sibfmbl ⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝑀 MblFnM 𝑆 ) )
22 1 2 3 4 5 6 7 8 9 sibfrn ⊢ ( 𝜑 → ran 𝐹 ∈ Fin )
23 1 2 3 4 5 6 7 8 9 sibfima ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑀 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) )
24 23 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) )
25 21 22 24 jca32 ⊢ ( 𝜑 → ( 𝐹 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∧ ( ran 𝐹 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) )
26 rneq ⊢ ( 𝑔 = 𝐹 → ran 𝑔 = ran 𝐹 )
27 26 eleq1d ⊢ ( 𝑔 = 𝐹 → ( ran 𝑔 ∈ Fin ↔ ran 𝐹 ∈ Fin ) )
28 26 difeq1d ⊢ ( 𝑔 = 𝐹 → ( ran 𝑔 ∖ { 0 } ) = ( ran 𝐹 ∖ { 0 } ) )
29 cnveq ⊢ ( 𝑔 = 𝐹 → ◡ 𝑔 = ◡ 𝐹 )
30 29 imaeq1d ⊢ ( 𝑔 = 𝐹 → ( ◡ 𝑔 “ { 𝑥 } ) = ( ◡ 𝐹 “ { 𝑥 } ) )
31 30 fveq2d ⊢ ( 𝑔 = 𝐹 → ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) = ( 𝑀 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) )
32 31 eleq1d ⊢ ( 𝑔 = 𝐹 → ( ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ↔ ( 𝑀 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) )
33 28 32 raleqbidv ⊢ ( 𝑔 = 𝐹 → ( ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ↔ ∀ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) )
34 27 33 anbi12d ⊢ ( 𝑔 = 𝐹 → ( ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ↔ ( ran 𝐹 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) )
35 34 elrab ⊢ ( 𝐹 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↔ ( 𝐹 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∧ ( ran 𝐹 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) )
36 25 35 sylibr ⊢ ( 𝜑 → 𝐹 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } )
37 ovexd ⊢ ( 𝜑 → ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ∈ V )
38 10 20 36 37 fvmptd ⊢ ( 𝜑 → ( ( 𝑊 sitg 𝑀 ) ‘ 𝐹 ) = ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) )