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 = 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
Assertion 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

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