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