Definition df-sitm

Description: Define the integral metric for simple functions, as the integral of the distances between the function values. Since distances take nonnegative values in RR* , the range structure for this integral is ` ( RR*s |``s ( 0 , +oo ) ) ` . See definition 2.3.1 of Bogachev p. 116. (Contributed by Thierry Arnoux, 22-Oct-2017)

	Ref	Expression
Assertion	df-sitm	⊢ sitm = ( 𝑤 ∈ V , 𝑚 ∈ ∪ ran measures ↦ ( 𝑓 ∈ dom ( 𝑤 sitg 𝑚 ) , 𝑔 ∈ dom ( 𝑤 sitg 𝑚 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑤 ) 𝑔 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csitm	⊢ sitm
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vm	⊢ 𝑚
4		cmeas	⊢ measures
5	4	crn	⊢ ran measures
6	5	cuni	⊢ ∪ ran measures
7		vf	⊢ 𝑓
8	1	cv	⊢ 𝑤
9		csitg	⊢ sitg
10	3	cv	⊢ 𝑚
11	8 10 9	co	⊢ ( 𝑤 sitg 𝑚 )
12	11	cdm	⊢ dom ( 𝑤 sitg 𝑚 )
13		vg	⊢ 𝑔
14		cxrs	⊢ ℝ*𝑠
15		cress	⊢ ↾s
16		cc0	⊢ 0
17		cicc	⊢ [,]
18		cpnf	⊢ +∞
19	16 18 17	co	⊢ ( 0 [,] +∞ )
20	14 19 15	co	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
21	20 10 9	co	⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 )
22	7	cv	⊢ 𝑓
23		cds	⊢ dist
24	8 23	cfv	⊢ ( dist ‘ 𝑤 )
25	24	cof	⊢ ∘f ( dist ‘ 𝑤 )
26	13	cv	⊢ 𝑔
27	22 26 25	co	⊢ ( 𝑓 ∘f ( dist ‘ 𝑤 ) 𝑔 )
28	27 21	cfv	⊢ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑤 ) 𝑔 ) )
29	7 13 12 12 28	cmpo	⊢ ( 𝑓 ∈ dom ( 𝑤 sitg 𝑚 ) , 𝑔 ∈ dom ( 𝑤 sitg 𝑚 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑤 ) 𝑔 ) ) )
30	1 3 2 6 29	cmpo	⊢ ( 𝑤 ∈ V , 𝑚 ∈ ∪ ran measures ↦ ( 𝑓 ∈ dom ( 𝑤 sitg 𝑚 ) , 𝑔 ∈ dom ( 𝑤 sitg 𝑚 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑤 ) 𝑔 ) ) ) )
31	0 30	wceq	⊢ sitm = ( 𝑤 ∈ V , 𝑚 ∈ ∪ ran measures ↦ ( 𝑓 ∈ dom ( 𝑤 sitg 𝑚 ) , 𝑔 ∈ dom ( 𝑤 sitg 𝑚 ) ↦ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) sitg 𝑚 ) ‘ ( 𝑓 ∘f ( dist ‘ 𝑤 ) 𝑔 ) ) ) )