Metamath Proof Explorer

Theorem sitmf

Description: The integral metric as a function. (Contributed by Thierry Arnoux, 13-Mar-2018)

Ref Expression
Hypotheses sitmf.0 
|- ( ph -> W e. Mnd )
sitmf.1 
|- ( ph -> W e. *MetSp )
sitmf.2 
|- ( ph -> M e. U. ran measures )
Assertion sitmf 
|- ( ph -> ( W sitm M ) : ( dom ( W sitg M ) X. dom ( W sitg M ) ) --> ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 sitmf.0 
 |-  ( ph -> W e. Mnd )
2 sitmf.1 
 |-  ( ph -> W e. *MetSp )
3 sitmf.2 
 |-  ( ph -> M e. U. ran measures )
4 eqid 
 |-  ( dist ` W ) = ( dist ` W )
5 2 adantr 
 |-  ( ( ph /\ ( f e. dom ( W sitg M ) /\ g e. dom ( W sitg M ) ) ) -> W e. *MetSp )
6 3 adantr 
 |-  ( ( ph /\ ( f e. dom ( W sitg M ) /\ g e. dom ( W sitg M ) ) ) -> M e. U. ran measures )
7 simprl 
 |-  ( ( ph /\ ( f e. dom ( W sitg M ) /\ g e. dom ( W sitg M ) ) ) -> f e. dom ( W sitg M ) )
8 simprr 
 |-  ( ( ph /\ ( f e. dom ( W sitg M ) /\ g e. dom ( W sitg M ) ) ) -> g e. dom ( W sitg M ) )
9 4 5 6 7 8 sitmfval 
 |-  ( ( ph /\ ( f e. dom ( W sitg M ) /\ g e. dom ( W sitg M ) ) ) -> ( f ( W sitm M ) g ) = ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF ( dist ` W ) g ) ) )
10 1 adantr 
 |-  ( ( ph /\ ( f e. dom ( W sitg M ) /\ g e. dom ( W sitg M ) ) ) -> W e. Mnd )
11 10 5 6 7 8 sitmcl 
 |-  ( ( ph /\ ( f e. dom ( W sitg M ) /\ g e. dom ( W sitg M ) ) ) -> ( f ( W sitm M ) g ) e. ( 0 [,] +oo ) )
12 9 11 eqeltrrd 
 |-  ( ( ph /\ ( f e. dom ( W sitg M ) /\ g e. dom ( W sitg M ) ) ) -> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF ( dist ` W ) g ) ) e. ( 0 [,] +oo ) )
13 12 ralrimivva 
 |-  ( ph -> A. f e. dom ( W sitg M ) A. g e. dom ( W sitg M ) ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF ( dist ` W ) g ) ) e. ( 0 [,] +oo ) )
14 eqid 
 |-  ( f e. dom ( W sitg M ) , g e. dom ( W sitg M ) |-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF ( dist ` W ) g ) ) ) = ( f e. dom ( W sitg M ) , g e. dom ( W sitg M ) |-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF ( dist ` W ) g ) ) )
15 14 fmpo 
 |-  ( A. f e. dom ( W sitg M ) A. g e. dom ( W sitg M ) ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF ( dist ` W ) g ) ) e. ( 0 [,] +oo ) <-> ( f e. dom ( W sitg M ) , g e. dom ( W sitg M ) |-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF ( dist ` W ) g ) ) ) : ( dom ( W sitg M ) X. dom ( W sitg M ) ) --> ( 0 [,] +oo ) )
16 13 15 sylib 
 |-  ( ph -> ( f e. dom ( W sitg M ) , g e. dom ( W sitg M ) |-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF ( dist ` W ) g ) ) ) : ( dom ( W sitg M ) X. dom ( W sitg M ) ) --> ( 0 [,] +oo ) )
17 4 2 3 sitmval 
 |-  ( ph -> ( W sitm M ) = ( f e. dom ( W sitg M ) , g e. dom ( W sitg M ) |-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF ( dist ` W ) g ) ) ) )
18 17 feq1d 
 |-  ( ph -> ( ( W sitm M ) : ( dom ( W sitg M ) X. dom ( W sitg M ) ) --> ( 0 [,] +oo ) <-> ( f e. dom ( W sitg M ) , g e. dom ( W sitg M ) |-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF ( dist ` W ) g ) ) ) : ( dom ( W sitg M ) X. dom ( W sitg M ) ) --> ( 0 [,] +oo ) ) )
19 16 18 mpbird 
 |-  ( ph -> ( W sitm M ) : ( dom ( W sitg M ) X. dom ( W sitg M ) ) --> ( 0 [,] +oo ) )