Metamath Proof Explorer


Definition df-sitg

Description: Define the integral of simple functions from a measurable space dom m to a generic space w equipped with the right scalar product. w will later be required to be a Banach space.

These simple functions are required to take finitely many different values: this is expressed by ran g e. Fin in the definition.

Moreover, for each x , the pre-image (`' g " { x } ) is requested to be measurable, of finite measure.

In this definition, ( sigaGen `( TopOpenw ) ) is the Borel sigma-algebra on w , and the functions g range over the measurable functions over that Borel algebra.

Definition 2.4.1 of Bogachev p. 118. (Contributed by Thierry Arnoux, 21-Oct-2017)

Ref Expression
Assertion 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

Detailed syntax breakdown

Step Hyp Ref Expression
0 csitg class sitg
1 vw setvar w
2 cvv class V
3 vm setvar m
4 cmeas class measures
5 4 crn class ran measures
6 5 cuni class ran measures
7 vf setvar f
8 vg setvar g
9 3 cv setvar m
10 9 cdm class dom m
11 cmbfm class MblFn μ
12 csigagen class 𝛔
13 ctopn class TopOpen
14 1 cv setvar w
15 14 13 cfv class TopOpen w
16 15 12 cfv class 𝛔 TopOpen w
17 10 16 11 co class dom m MblFn μ 𝛔 TopOpen w
18 8 cv setvar g
19 18 crn class ran g
20 cfn class Fin
21 19 20 wcel wff ran g Fin
22 vx setvar x
23 c0g class 0 𝑔
24 14 23 cfv class 0 w
25 24 csn class 0 w
26 19 25 cdif class ran g 0 w
27 18 ccnv class g -1
28 22 cv setvar x
29 28 csn class x
30 27 29 cima class g -1 x
31 30 9 cfv class m g -1 x
32 cc0 class 0
33 cico class .
34 cpnf class +∞
35 32 34 33 co class 0 +∞
36 31 35 wcel wff m g -1 x 0 +∞
37 36 22 26 wral wff x ran g 0 w m g -1 x 0 +∞
38 21 37 wa wff ran g Fin x ran g 0 w m g -1 x 0 +∞
39 38 8 17 crab class g dom m MblFn μ 𝛔 TopOpen w | ran g Fin x ran g 0 w m g -1 x 0 +∞
40 cgsu class Σ𝑔
41 7 cv setvar f
42 41 crn class ran f
43 42 25 cdif class ran f 0 w
44 crrh class ℝHom
45 csca class Scalar
46 14 45 cfv class Scalar w
47 46 44 cfv class ℝHom Scalar w
48 41 ccnv class f -1
49 48 29 cima class f -1 x
50 49 9 cfv class m f -1 x
51 50 47 cfv class ℝHom Scalar w m f -1 x
52 cvsca class 𝑠
53 14 52 cfv class w
54 51 28 53 co class ℝHom Scalar w m f -1 x w x
55 22 43 54 cmpt class x ran f 0 w ℝHom Scalar w m f -1 x w x
56 14 55 40 co class w x ran f 0 w ℝHom Scalar w m f -1 x w x
57 7 39 56 cmpt class 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
58 1 3 2 6 57 cmpo class 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
59 0 58 wceq wff 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