Definition df-sitg 30392

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 ` ( TopOpen ` w ) ) 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.)

Assertion

Ref	Expression
df-sitg	|- sitg = ( w e. _V , m e. U. ran measures |-> ( f e. { g e. ( dom mMblFnM (sigaGen ` ( TopOpen ` w ) ) ) | ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( w gsumg ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( (RRHom ` (Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) ) ) ) )

Distinct variable group:   f, g, m, w, x

Detailed syntax breakdown of Definition df-sitg

Step	Hyp	Ref	Expression
1		csitg 30391	. 2 class sitg
2		vw	. . 3 setvar w
3		vm	. . 3 setvar m
4		cvv 3200	. . 3 class _V
5		cmeas 30258	. . . . 5 class measures
6	5	crn 5115	. . . 4 class ran measures
7	6	cuni 4436	. . 3 class U. ran measures
8		vf	. . . 4 setvar f
9		vg	. . . . . . . . 9 setvar g
10	9	cv 1482	. . . . . . . 8 class g
11	10	crn 5115	. . . . . . 7 class ran g
12		cfn 7955	. . . . . . 7 class Fin
13	11, 12	wcel 1990	. . . . . 6 wff ran g e. Fin
14	10	ccnv 5113	. . . . . . . . . 10 class `' g
15		vx	. . . . . . . . . . . 12 setvar x
16	15	cv 1482	. . . . . . . . . . 11 class x
17	16	csn 4177	. . . . . . . . . 10 class { x }
18	14, 17	cima 5117	. . . . . . . . 9 class ( `' g " { x } )
19	3	cv 1482	. . . . . . . . 9 class m
20	18, 19	cfv 5888	. . . . . . . 8 class ( m ` ( `' g " { x } ) )
21		cc0 9936	. . . . . . . . 9 class 0
22		cpnf 10071	. . . . . . . . 9 class +oo
23		cico 12177	. . . . . . . . 9 class [,)
24	21, 22, 23	co 6650	. . . . . . . 8 class ( 0 [,) +oo )
25	20, 24	wcel 1990	. . . . . . 7 wff ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo )
26	2	cv 1482	. . . . . . . . . 10 class w
27		c0g 16100	. . . . . . . . . 10 class 0g
28	26, 27	cfv 5888	. . . . . . . . 9 class ( 0g ` w )
29	28	csn 4177	. . . . . . . 8 class { ( 0g ` w ) }
30	11, 29	cdif 3571	. . . . . . 7 class ( ran g \ { ( 0g ` w ) } )
31	25, 15, 30	wral 2912	. . . . . 6 wff A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo )
32	13, 31	wa 384	. . . . 5 wff ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) )
33	19	cdm 5114	. . . . . 6 class dom m
34		ctopn 16082	. . . . . . . 8 class TopOpen
35	26, 34	cfv 5888	. . . . . . 7 class ( TopOpen ` w )
36		csigagen 30201	. . . . . . 7 class sigaGen
37	35, 36	cfv 5888	. . . . . 6 class (sigaGen ` ( TopOpen ` w ) )
38		cmbfm 30312	. . . . . 6 class MblFnM
39	33, 37, 38	co 6650	. . . . 5 class ( dom mMblFnM (sigaGen ` ( TopOpen ` w ) ) )
40	32, 9, 39	crab 2916	. . . 4 class { g e. ( dom mMblFnM (sigaGen ` ( TopOpen ` w ) ) ) | ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) }
41	8	cv 1482	. . . . . . . 8 class f
42	41	crn 5115	. . . . . . 7 class ran f
43	42, 29	cdif 3571	. . . . . 6 class ( ran f \ { ( 0g ` w ) } )
44	41	ccnv 5113	. . . . . . . . . 10 class `' f
45	44, 17	cima 5117	. . . . . . . . 9 class ( `' f " { x } )
46	45, 19	cfv 5888	. . . . . . . 8 class ( m ` ( `' f " { x } ) )
47		csca 15944	. . . . . . . . . 10 class Scalar
48	26, 47	cfv 5888	. . . . . . . . 9 class (Scalar ` w )
49		crrh 30037	. . . . . . . . 9 class RRHom
50	48, 49	cfv 5888	. . . . . . . 8 class (RRHom ` (Scalar ` w ) )
51	46, 50	cfv 5888	. . . . . . 7 class ( (RRHom ` (Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) )
52		cvsca 15945	. . . . . . . 8 class .s
53	26, 52	cfv 5888	. . . . . . 7 class ( .s ` w )
54	51, 16, 53	co 6650	. . . . . 6 class ( ( (RRHom ` (Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x )
55	15, 43, 54	cmpt 4729	. . . . 5 class ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( (RRHom ` (Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) )
56		cgsu 16101	. . . . 5 class gsumg
57	26, 55, 56	co 6650	. . . 4 class ( w gsumg ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( (RRHom ` (Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) ) )
58	8, 40, 57	cmpt 4729	. . 3 class ( f e. { g e. ( dom mMblFnM (sigaGen ` ( TopOpen ` w ) ) ) | ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( w gsumg ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( (RRHom ` (Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) ) ) )
59	2, 3, 4, 7, 58	cmpt2 6652	. 2 class ( w e. _V , m e. U. ran measures |-> ( f e. { g e. ( dom mMblFnM (sigaGen ` ( TopOpen ` w ) ) ) | ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( w gsumg ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( (RRHom ` (Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) ) ) ) )
60	1, 59	wceq 1483	1 wff sitg = ( w e. _V , m e. U. ran measures |-> ( f e. { g e. ( dom mMblFnM (sigaGen ` ( TopOpen ` w ) ) ) | ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( w gsumg ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( (RRHom ` (Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) ) ) ) )

This definition is referenced by:  sitgval  30394