Definition df-sitg 34367

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

Step	Hyp	Ref	Expression
1		csitg 34366	. 2 class sitg
2		vw	. . 3 setvar 𝑤
3		vm	. . 3 setvar 𝑚
4		cvv 3464	. . 3 class V
5		cmeas 34231	. . . . 5 class measures
6	5	crn 5660	. . . 4 class ran measures
7	6	cuni 4888	. . 3 class ∪ ran measures
8		vf	. . . 4 setvar 𝑓
9		vg	. . . . . . . . 9 setvar 𝑔
10	9	cv 1539	. . . . . . . 8 class 𝑔
11	10	crn 5660	. . . . . . 7 class ran 𝑔
12		cfn 8964	. . . . . . 7 class Fin
13	11, 12	wcel 2109	. . . . . 6 wff ran 𝑔 ∈ Fin
14	10	ccnv 5658	. . . . . . . . . 10 class ◡𝑔
15		vx	. . . . . . . . . . . 12 setvar 𝑥
16	15	cv 1539	. . . . . . . . . . 11 class 𝑥
17	16	csn 4606	. . . . . . . . . 10 class {𝑥}
18	14, 17	cima 5662	. . . . . . . . 9 class (◡𝑔 “ {𝑥})
19	3	cv 1539	. . . . . . . . 9 class 𝑚
20	18, 19	cfv 6536	. . . . . . . 8 class (𝑚‘(◡𝑔 “ {𝑥}))
21		cc0 11134	. . . . . . . . 9 class 0
22		cpnf 11271	. . . . . . . . 9 class +∞
23		cico 13369	. . . . . . . . 9 class [,)
24	21, 22, 23	co 7410	. . . . . . . 8 class (0[,)+∞)
25	20, 24	wcel 2109	. . . . . . 7 wff (𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)
26	2	cv 1539	. . . . . . . . . 10 class 𝑤
27		c0g 17458	. . . . . . . . . 10 class 0g
28	26, 27	cfv 6536	. . . . . . . . 9 class (0g‘𝑤)
29	28	csn 4606	. . . . . . . 8 class {(0g‘𝑤)}
30	11, 29	cdif 3928	. . . . . . 7 class (ran 𝑔 ∖ {(0g‘𝑤)})
31	25, 15, 30	wral 3052	. . . . . 6 wff ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)
32	13, 31	wa 395	. . . . 5 wff (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))
33	19	cdm 5659	. . . . . 6 class dom 𝑚
34		ctopn 17440	. . . . . . . 8 class TopOpen
35	26, 34	cfv 6536	. . . . . . 7 class (TopOpen‘𝑤)
36		csigagen 34174	. . . . . . 7 class sigaGen
37	35, 36	cfv 6536	. . . . . 6 class (sigaGen‘(TopOpen‘𝑤))
38		cmbfm 34285	. . . . . 6 class MblFnM
39	33, 37, 38	co 7410	. . . . 5 class (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤)))
40	32, 9, 39	crab 3420	. . . 4 class {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))}
41	8	cv 1539	. . . . . . . 8 class 𝑓
42	41	crn 5660	. . . . . . 7 class ran 𝑓
43	42, 29	cdif 3928	. . . . . 6 class (ran 𝑓 ∖ {(0g‘𝑤)})
44	41	ccnv 5658	. . . . . . . . . 10 class ◡𝑓
45	44, 17	cima 5662	. . . . . . . . 9 class (◡𝑓 “ {𝑥})
46	45, 19	cfv 6536	. . . . . . . 8 class (𝑚‘(◡𝑓 “ {𝑥}))
47		csca 17279	. . . . . . . . . 10 class Scalar
48	26, 47	cfv 6536	. . . . . . . . 9 class (Scalar‘𝑤)
49		crrh 34029	. . . . . . . . 9 class ℝHom
50	48, 49	cfv 6536	. . . . . . . 8 class (ℝHom‘(Scalar‘𝑤))
51	46, 50	cfv 6536	. . . . . . 7 class ((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))
52		cvsca 17280	. . . . . . . 8 class ·𝑠
53	26, 52	cfv 6536	. . . . . . 7 class ( ·𝑠 ‘𝑤)
54	51, 16, 53	co 7410	. . . . . 6 class (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)
55	15, 43, 54	cmpt 5206	. . . . 5 class (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥))
56		cgsu 17459	. . . . 5 class Σg
57	26, 55, 56	co 7410	. . . 4 class (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)))
58	8, 40, 57	cmpt 5206	. . 3 class (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥))))
59	2, 3, 4, 7, 58	cmpo 7412	. 2 class (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)))))
60	1, 59	wceq 1540	1 wff sitg = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)))))

This definition is referenced by:  sitgval  34369