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 = ( 𝑤 ∈ V , 𝑚 ran measures ↦ ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g𝑤 ) } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠𝑤 ) 𝑥 ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csitg sitg
1 vw 𝑤
2 cvv V
3 vm 𝑚
4 cmeas measures
5 4 crn ran measures
6 5 cuni ran measures
7 vf 𝑓
8 vg 𝑔
9 3 cv 𝑚
10 9 cdm dom 𝑚
11 cmbfm MblFnM
12 csigagen sigaGen
13 ctopn TopOpen
14 1 cv 𝑤
15 14 13 cfv ( TopOpen ‘ 𝑤 )
16 15 12 cfv ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) )
17 10 16 11 co ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) )
18 8 cv 𝑔
19 18 crn ran 𝑔
20 cfn Fin
21 19 20 wcel ran 𝑔 ∈ Fin
22 vx 𝑥
23 c0g 0g
24 14 23 cfv ( 0g𝑤 )
25 24 csn { ( 0g𝑤 ) }
26 19 25 cdif ( ran 𝑔 ∖ { ( 0g𝑤 ) } )
27 18 ccnv 𝑔
28 22 cv 𝑥
29 28 csn { 𝑥 }
30 27 29 cima ( 𝑔 “ { 𝑥 } )
31 30 9 cfv ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) )
32 cc0 0
33 cico [,)
34 cpnf +∞
35 32 34 33 co ( 0 [,) +∞ )
36 31 35 wcel ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ )
37 36 22 26 wral 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g𝑤 ) } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ )
38 21 37 wa ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g𝑤 ) } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) )
39 38 8 17 crab { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g𝑤 ) } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) }
40 cgsu Σg
41 7 cv 𝑓
42 41 crn ran 𝑓
43 42 25 cdif ( ran 𝑓 ∖ { ( 0g𝑤 ) } )
44 crrh ℝHom
45 csca Scalar
46 14 45 cfv ( Scalar ‘ 𝑤 )
47 46 44 cfv ( ℝHom ‘ ( Scalar ‘ 𝑤 ) )
48 41 ccnv 𝑓
49 48 29 cima ( 𝑓 “ { 𝑥 } )
50 49 9 cfv ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) )
51 50 47 cfv ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) )
52 cvsca ·𝑠
53 14 52 cfv ( ·𝑠𝑤 )
54 51 28 53 co ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠𝑤 ) 𝑥 )
55 22 43 54 cmpt ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠𝑤 ) 𝑥 ) )
56 14 55 40 co ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠𝑤 ) 𝑥 ) ) )
57 7 39 56 cmpt ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g𝑤 ) } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠𝑤 ) 𝑥 ) ) ) )
58 1 3 2 6 57 cmpo ( 𝑤 ∈ V , 𝑚 ran measures ↦ ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g𝑤 ) } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠𝑤 ) 𝑥 ) ) ) ) )
59 0 58 wceq sitg = ( 𝑤 ∈ V , 𝑚 ran measures ↦ ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g𝑤 ) } ) ( 𝑚 ‘ ( 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠𝑤 ) 𝑥 ) ) ) ) )