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⁡mMblFnμ𝛔⁡TopOpen⁡w|ran⁡g∈Fin∧∀x∈ran⁡g∖0wm⁡g-1x∈0+∞⟼∑wx∈ran⁡f∖0wℝHom⁡Scalar⁡w⁡m⁡f-1x⋅wx

Detailed syntax breakdown

Step Hyp Ref Expression
0 csitg classsitg
1 vw setvarw
2 cvv classV
3 vm setvarm
4 cmeas classmeasures
5 4 crn classran⁡measures
6 5 cuni class⋃ran⁡measures
7 vf setvarf
8 vg setvarg
9 3 cv setvarm
10 9 cdm classdom⁡m
11 cmbfm classMblFnμ
12 csigagen class𝛔
13 ctopn classTopOpen
14 1 cv setvarw
15 14 13 cfv classTopOpen⁡w
16 15 12 cfv class𝛔⁡TopOpen⁡w
17 10 16 11 co classdom⁡mMblFnμ𝛔⁡TopOpen⁡w
18 8 cv setvarg
19 18 crn classran⁡g
20 cfn classFin
21 19 20 wcel wffran⁡g∈Fin
22 vx setvarx
23 c0g class0𝑔
24 14 23 cfv class0w
25 24 csn class0w
26 19 25 cdif classran⁡g∖0w
27 18 ccnv classg-1
28 22 cv setvarx
29 28 csn classx
30 27 29 cima classg-1x
31 30 9 cfv classm⁡g-1x
32 cc0 class0
33 cico class.
34 cpnf class+∞
35 32 34 33 co class0+∞
36 31 35 wcel wffm⁡g-1x∈0+∞
37 36 22 26 wral wff∀x∈ran⁡g∖0wm⁡g-1x∈0+∞
38 21 37 wa wffran⁡g∈Fin∧∀x∈ran⁡g∖0wm⁡g-1x∈0+∞
39 38 8 17 crab classg∈dom⁡mMblFnμ𝛔⁡TopOpen⁡w|ran⁡g∈Fin∧∀x∈ran⁡g∖0wm⁡g-1x∈0+∞
40 cgsu classΣ𝑔
41 7 cv setvarf
42 41 crn classran⁡f
43 42 25 cdif classran⁡f∖0w
44 crrh classℝHom
45 csca classScalar
46 14 45 cfv classScalar⁡w
47 46 44 cfv classℝHom⁡Scalar⁡w
48 41 ccnv classf-1
49 48 29 cima classf-1x
50 49 9 cfv classm⁡f-1x
51 50 47 cfv classℝHom⁡Scalar⁡w⁡m⁡f-1x
52 cvsca class⋅𝑠
53 14 52 cfv class⋅w
54 51 28 53 co classℝHom⁡Scalar⁡w⁡m⁡f-1x⋅wx
55 22 43 54 cmpt classx∈ran⁡f∖0w⟼ℝHom⁡Scalar⁡w⁡m⁡f-1x⋅wx
56 14 55 40 co class∑wx∈ran⁡f∖0wℝHom⁡Scalar⁡w⁡m⁡f-1x⋅wx
57 7 39 56 cmpt classf∈g∈dom⁡mMblFnμ𝛔⁡TopOpen⁡w|ran⁡g∈Fin∧∀x∈ran⁡g∖0wm⁡g-1x∈0+∞⟼∑wx∈ran⁡f∖0wℝHom⁡Scalar⁡w⁡m⁡f-1x⋅wx
58 1 3 2 6 57 cmpo classw∈V,m∈⋃ran⁡measures⟼f∈g∈dom⁡mMblFnμ𝛔⁡TopOpen⁡w|ran⁡g∈Fin∧∀x∈ran⁡g∖0wm⁡g-1x∈0+∞⟼∑wx∈ran⁡f∖0wℝHom⁡Scalar⁡w⁡m⁡f-1x⋅wx
59 0 58 wceq wffsitg=w∈V,m∈⋃ran⁡measures⟼f∈g∈dom⁡mMblFnμ𝛔⁡TopOpen⁡w|ran⁡g∈Fin∧∀x∈ran⁡g∖0wm⁡g-1x∈0+∞⟼∑wx∈ran⁡f∖0wℝHom⁡Scalar⁡w⁡m⁡f-1x⋅wx