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 ⊢ 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
sibfmbl.1 ⊢ φ → F ∈ ℑ M W
Assertion sitgfval ⊢ φ → ∫ ℑ W F dM = ∑ W x ∈ ran ⁡ F ∖ 0 ˙ H ⁡ M ⁡ F -1 x · ˙ x

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 sibfmbl.1 ⊢ φ → F ∈ ℑ M W
10 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
11 simpr ⊢ φ ∧ f = F → f = F
12 11 rneqd ⊢ φ ∧ f = F → ran ⁡ f = ran ⁡ F
13 12 difeq1d ⊢ φ ∧ f = F → ran ⁡ f ∖ 0 ˙ = ran ⁡ F ∖ 0 ˙
14 11 cnveqd ⊢ φ ∧ f = F → f -1 = F -1
15 14 imaeq1d ⊢ φ ∧ f = F → f -1 x = F -1 x
16 15 fveq2d ⊢ φ ∧ f = F → M ⁡ f -1 x = M ⁡ F -1 x
17 16 fveq2d ⊢ φ ∧ f = F → H ⁡ M ⁡ f -1 x = H ⁡ M ⁡ F -1 x
18 17 oveq1d ⊢ φ ∧ f = F → H ⁡ M ⁡ f -1 x · ˙ x = H ⁡ M ⁡ F -1 x · ˙ x
19 13 18 mpteq12dv ⊢ φ ∧ f = F → x ∈ ran ⁡ f ∖ 0 ˙ ⟼ H ⁡ M ⁡ f -1 x · ˙ x = x ∈ ran ⁡ F ∖ 0 ˙ ⟼ H ⁡ M ⁡ F -1 x · ˙ x
20 19 oveq2d ⊢ φ ∧ f = F → ∑ W x ∈ ran ⁡ f ∖ 0 ˙ H ⁡ M ⁡ f -1 x · ˙ x = ∑ W x ∈ ran ⁡ F ∖ 0 ˙ H ⁡ M ⁡ F -1 x · ˙ x
21 1 2 3 4 5 6 7 8 9 sibfmbl ⊢ φ → F ∈ dom ⁡ M MblFn μ S
22 1 2 3 4 5 6 7 8 9 sibfrn ⊢ φ → ran ⁡ F ∈ Fin
23 1 2 3 4 5 6 7 8 9 sibfima ⊢ φ ∧ x ∈ ran ⁡ F ∖ 0 ˙ → M ⁡ F -1 x ∈ 0 +∞
24 23 ralrimiva ⊢ φ → ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞
25 21 22 24 jca32 ⊢ φ → F ∈ dom ⁡ M MblFn μ S ∧ ran ⁡ F ∈ Fin ∧ ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞
26 rneq ⊢ g = F → ran ⁡ g = ran ⁡ F
27 26 eleq1d ⊢ g = F → ran ⁡ g ∈ Fin ↔ ran ⁡ F ∈ Fin
28 26 difeq1d ⊢ g = F → ran ⁡ g ∖ 0 ˙ = ran ⁡ F ∖ 0 ˙
29 cnveq ⊢ g = F → g -1 = F -1
30 29 imaeq1d ⊢ g = F → g -1 x = F -1 x
31 30 fveq2d ⊢ g = F → M ⁡ g -1 x = M ⁡ F -1 x
32 31 eleq1d ⊢ g = F → M ⁡ g -1 x ∈ 0 +∞ ↔ M ⁡ F -1 x ∈ 0 +∞
33 28 32 raleqbidv ⊢ g = F → ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ↔ ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞
34 27 33 anbi12d ⊢ g = F → ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ↔ ran ⁡ F ∈ Fin ∧ ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞
35 34 elrab ⊢ F ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞ ↔ F ∈ dom ⁡ M MblFn μ S ∧ ran ⁡ F ∈ Fin ∧ ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞
36 25 35 sylibr ⊢ φ → F ∈ g ∈ dom ⁡ M MblFn μ S | ran ⁡ g ∈ Fin ∧ ∀ x ∈ ran ⁡ g ∖ 0 ˙ M ⁡ g -1 x ∈ 0 +∞
37 ovexd ⊢ φ → ∑ W x ∈ ran ⁡ F ∖ 0 ˙ H ⁡ M ⁡ F -1 x · ˙ x ∈ V
38 10 20 36 37 fvmptd ⊢ φ → ∫ ℑ W F dM = ∑ W x ∈ ran ⁡ F ∖ 0 ˙ H ⁡ M ⁡ F -1 x · ˙ x