Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sitg Structured version   Visualization version   GIF version

Definition df-sitg 29719
 Description: Define the integral of simple functions from a measurable space dom 𝑚 to a generic space 𝑤 equipped with the right scalar product. 𝑤 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 𝑔 ∈ Fin in the definition. Moreover, for each 𝑥, the pre-image (◡𝑔 “ {𝑥}) is requested to be measurable, of finite measure. In this definition, (sigaGen‘(TopOpen‘𝑤)) is the Borel sigma-algebra on 𝑤, and the functions 𝑔 range over the measurable functions over that Borel algebra. Definition 2.4.1 of [Bogachev] p. 118. (Contributed by Thierry Arnoux, 21-Oct-2017.)
Assertion
Ref Expression
df-sitg sitg = (𝑤 ∈ V, 𝑚 ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)))))
Distinct variable group:   𝑓,𝑔,𝑚,𝑤,𝑥

Detailed syntax breakdown of Definition df-sitg
StepHypRef Expression
1 csitg 29718 . 2 class sitg
2 vw . . 3 setvar 𝑤
3 vm . . 3 setvar 𝑚
4 cvv 3173 . . 3 class V
5 cmeas 29585 . . . . 5 class measures
65crn 5039 . . . 4 class ran measures
76cuni 4372 . . 3 class ran measures
8 vf . . . 4 setvar 𝑓
9 vg . . . . . . . . 9 setvar 𝑔
109cv 1474 . . . . . . . 8 class 𝑔
1110crn 5039 . . . . . . 7 class ran 𝑔
12 cfn 7841 . . . . . . 7 class Fin
1311, 12wcel 1977 . . . . . 6 wff ran 𝑔 ∈ Fin
1410ccnv 5037 . . . . . . . . . 10 class 𝑔
15 vx . . . . . . . . . . . 12 setvar 𝑥
1615cv 1474 . . . . . . . . . . 11 class 𝑥
1716csn 4125 . . . . . . . . . 10 class {𝑥}
1814, 17cima 5041 . . . . . . . . 9 class (𝑔 “ {𝑥})
193cv 1474 . . . . . . . . 9 class 𝑚
2018, 19cfv 5804 . . . . . . . 8 class (𝑚‘(𝑔 “ {𝑥}))
21 cc0 9815 . . . . . . . . 9 class 0
22 cpnf 9950 . . . . . . . . 9 class +∞
23 cico 12048 . . . . . . . . 9 class [,)
2421, 22, 23co 6549 . . . . . . . 8 class (0[,)+∞)
2520, 24wcel 1977 . . . . . . 7 wff (𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞)
262cv 1474 . . . . . . . . . 10 class 𝑤
27 c0g 15923 . . . . . . . . . 10 class 0g
2826, 27cfv 5804 . . . . . . . . 9 class (0g𝑤)
2928csn 4125 . . . . . . . 8 class {(0g𝑤)}
3011, 29cdif 3537 . . . . . . 7 class (ran 𝑔 ∖ {(0g𝑤)})
3125, 15, 30wral 2896 . . . . . 6 wff 𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞)
3213, 31wa 383 . . . . 5 wff (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))
3319cdm 5038 . . . . . 6 class dom 𝑚
34 ctopn 15905 . . . . . . . 8 class TopOpen
3526, 34cfv 5804 . . . . . . 7 class (TopOpen‘𝑤)
36 csigagen 29528 . . . . . . 7 class sigaGen
3735, 36cfv 5804 . . . . . 6 class (sigaGen‘(TopOpen‘𝑤))
38 cmbfm 29639 . . . . . 6 class MblFnM
3933, 37, 38co 6549 . . . . 5 class (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤)))
4032, 9, 39crab 2900 . . . 4 class {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))}
418cv 1474 . . . . . . . 8 class 𝑓
4241crn 5039 . . . . . . 7 class ran 𝑓
4342, 29cdif 3537 . . . . . 6 class (ran 𝑓 ∖ {(0g𝑤)})
4441ccnv 5037 . . . . . . . . . 10 class 𝑓
4544, 17cima 5041 . . . . . . . . 9 class (𝑓 “ {𝑥})
4645, 19cfv 5804 . . . . . . . 8 class (𝑚‘(𝑓 “ {𝑥}))
47 csca 15771 . . . . . . . . . 10 class Scalar
4826, 47cfv 5804 . . . . . . . . 9 class (Scalar‘𝑤)
49 crrh 29365 . . . . . . . . 9 class ℝHom
5048, 49cfv 5804 . . . . . . . 8 class (ℝHom‘(Scalar‘𝑤))
5146, 50cfv 5804 . . . . . . 7 class ((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))
52 cvsca 15772 . . . . . . . 8 class ·𝑠
5326, 52cfv 5804 . . . . . . 7 class ( ·𝑠𝑤)
5451, 16, 53co 6549 . . . . . 6 class (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)
5515, 43, 54cmpt 4643 . . . . 5 class (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥))
56 cgsu 15924 . . . . 5 class Σg
5726, 55, 56co 6549 . . . 4 class (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)))
588, 40, 57cmpt 4643 . . 3 class (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥))))
592, 3, 4, 7, 58cmpt2 6551 . 2 class (𝑤 ∈ V, 𝑚 ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)))))
601, 59wceq 1475 1 wff sitg = (𝑤 ∈ V, 𝑚 ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)))))
 Colors of variables: wff setvar class This definition is referenced by:  sitgval  29721
 Copyright terms: Public domain W3C validator