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 = ( w e. _V , m e. U. ran measures |-> ( f e. dom ( w sitg m ) , g e. dom ( w sitg m ) |-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg m ) ` ( f oF ( dist ` w ) g ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csitm 
 |-  sitm
1 vw 
 |-  w
2 cvv 
 |-  _V
3 vm 
 |-  m
4 cmeas 
 |-  measures
5 4 crn 
 |-  ran measures
6 5 cuni 
 |-  U. ran measures
7 vf 
 |-  f
8 1 cv 
 |-  w
9 csitg 
 |-  sitg
10 3 cv 
 |-  m
11 8 10 9 co 
 |-  ( w sitg m )
12 11 cdm 
 |-  dom ( w sitg m )
13 vg 
 |-  g
14 cxrs 
 |-  RR*s
15 cress 
 |-  |`s
16 cc0 
 |-  0
17 cicc 
 |-  [,]
18 cpnf 
 |-  +oo
19 16 18 17 co 
 |-  ( 0 [,] +oo )
20 14 19 15 co 
 |-  ( RR*s |`s ( 0 [,] +oo ) )
21 20 10 9 co 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) sitg m )
22 7 cv 
 |-  f
23 cds 
 |-  dist
24 8 23 cfv 
 |-  ( dist ` w )
25 24 cof 
 |-  oF ( dist ` w )
26 13 cv 
 |-  g
27 22 26 25 co 
 |-  ( f oF ( dist ` w ) g )
28 27 21 cfv 
 |-  ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg m ) ` ( f oF ( dist ` w ) g ) )
29 7 13 12 12 28 cmpo 
 |-  ( f e. dom ( w sitg m ) , g e. dom ( w sitg m ) |-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg m ) ` ( f oF ( dist ` w ) g ) ) )
30 1 3 2 6 29 cmpo 
 |-  ( w e. _V , m e. U. ran measures |-> ( f e. dom ( w sitg m ) , g e. dom ( w sitg m ) |-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg m ) ` ( f oF ( dist ` w ) g ) ) ) )
31 0 30 wceq 
 |-  sitm = ( w e. _V , m e. U. ran measures |-> ( f e. dom ( w sitg m ) , g e. dom ( w sitg m ) |-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg m ) ` ( f oF ( dist ` w ) g ) ) ) )