Definition df-sitg 31588

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 31587	. 2 class sitg
2		vw	. . 3 setvar 𝑤
3		vm	. . 3 setvar 𝑚
4		cvv 3494	. . 3 class V
5		cmeas 31454	. . . . 5 class measures
6	5	crn 5555	. . . 4 class ran measures
7	6	cuni 4837	. . 3 class ∪ ran measures
8		vf	. . . 4 setvar 𝑓
9		vg	. . . . . . . . 9 setvar 𝑔
10	9	cv 1532	. . . . . . . 8 class 𝑔
11	10	crn 5555	. . . . . . 7 class ran 𝑔
12		cfn 8508	. . . . . . 7 class Fin
13	11, 12	wcel 2110	. . . . . 6 wff ran 𝑔 ∈ Fin
14	10	ccnv 5553	. . . . . . . . . 10 class ◡𝑔
15		vx	. . . . . . . . . . . 12 setvar 𝑥
16	15	cv 1532	. . . . . . . . . . 11 class 𝑥
17	16	csn 4566	. . . . . . . . . 10 class {𝑥}
18	14, 17	cima 5557	. . . . . . . . 9 class (◡𝑔 “ {𝑥})
19	3	cv 1532	. . . . . . . . 9 class 𝑚
20	18, 19	cfv 6354	. . . . . . . 8 class (𝑚‘(◡𝑔 “ {𝑥}))
21		cc0 10536	. . . . . . . . 9 class 0
22		cpnf 10671	. . . . . . . . 9 class +∞
23		cico 12739	. . . . . . . . 9 class [,)
24	21, 22, 23	co 7155	. . . . . . . 8 class (0[,)+∞)
25	20, 24	wcel 2110	. . . . . . 7 wff (𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)
26	2	cv 1532	. . . . . . . . . 10 class 𝑤
27		c0g 16712	. . . . . . . . . 10 class 0g
28	26, 27	cfv 6354	. . . . . . . . 9 class (0g‘𝑤)
29	28	csn 4566	. . . . . . . 8 class {(0g‘𝑤)}
30	11, 29	cdif 3932	. . . . . . 7 class (ran 𝑔 ∖ {(0g‘𝑤)})
31	25, 15, 30	wral 3138	. . . . . 6 wff ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)
32	13, 31	wa 398	. . . . 5 wff (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))
33	19	cdm 5554	. . . . . 6 class dom 𝑚
34		ctopn 16694	. . . . . . . 8 class TopOpen
35	26, 34	cfv 6354	. . . . . . 7 class (TopOpen‘𝑤)
36		csigagen 31397	. . . . . . 7 class sigaGen
37	35, 36	cfv 6354	. . . . . 6 class (sigaGen‘(TopOpen‘𝑤))
38		cmbfm 31508	. . . . . 6 class MblFnM
39	33, 37, 38	co 7155	. . . . 5 class (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤)))
40	32, 9, 39	crab 3142	. . . 4 class {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))}
41	8	cv 1532	. . . . . . . 8 class 𝑓
42	41	crn 5555	. . . . . . 7 class ran 𝑓
43	42, 29	cdif 3932	. . . . . 6 class (ran 𝑓 ∖ {(0g‘𝑤)})
44	41	ccnv 5553	. . . . . . . . . 10 class ◡𝑓
45	44, 17	cima 5557	. . . . . . . . 9 class (◡𝑓 “ {𝑥})
46	45, 19	cfv 6354	. . . . . . . 8 class (𝑚‘(◡𝑓 “ {𝑥}))
47		csca 16567	. . . . . . . . . 10 class Scalar
48	26, 47	cfv 6354	. . . . . . . . 9 class (Scalar‘𝑤)
49		crrh 31234	. . . . . . . . 9 class ℝHom
50	48, 49	cfv 6354	. . . . . . . 8 class (ℝHom‘(Scalar‘𝑤))
51	46, 50	cfv 6354	. . . . . . 7 class ((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))
52		cvsca 16568	. . . . . . . 8 class ·𝑠
53	26, 52	cfv 6354	. . . . . . 7 class ( ·𝑠 ‘𝑤)
54	51, 16, 53	co 7155	. . . . . 6 class (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)
55	15, 43, 54	cmpt 5145	. . . . 5 class (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥))
56		cgsu 16713	. . . . 5 class Σg
57	26, 55, 56	co 7155	. . . 4 class (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)))
58	8, 40, 57	cmpt 5145	. . 3 class (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥))))
59	2, 3, 4, 7, 58	cmpo 7157	. 2 class (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)))))
60	1, 59	wceq 1533	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  31590