Metamath Proof Explorer


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 ‘ 𝑤 ) 𝑔 ) ) ) )