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