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 ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ) ) ) )