Metamath Proof Explorer

Theorem sitmval

Description: Value of the simple function integral metric for a given space W and measure M . (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses sitmval.d 
|- D = ( dist ` W )
sitmval.1 
|- ( ph -> W e. V )
sitmval.2 
|- ( ph -> M e. U. ran measures )
Assertion 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 D g ) ) ) )

Proof

Step Hyp Ref Expression
1 sitmval.d 
 |-  D = ( dist ` W )
2 sitmval.1 
 |-  ( ph -> W e. V )
3 sitmval.2 
 |-  ( ph -> M e. U. ran measures )
4 elex 
 |-  ( W e. V -> W e. _V )
5 2 4 syl 
 |-  ( ph -> W e. _V )
6 oveq1 
 |-  ( w = W -> ( w sitg m ) = ( W sitg m ) )
7 6 dmeqd 
 |-  ( w = W -> dom ( w sitg m ) = dom ( W sitg m ) )
8 fveq2 
 |-  ( w = W -> ( dist ` w ) = ( dist ` W ) )
9 ofeq 
 |-  ( ( dist ` w ) = ( dist ` W ) -> oF ( dist ` w ) = oF ( dist ` W ) )
10 8 9 syl 
 |-  ( w = W -> oF ( dist ` w ) = oF ( dist ` W ) )
11 10 oveqd 
 |-  ( w = W -> ( f oF ( dist ` w ) g ) = ( f oF ( dist ` W ) g ) )
12 11 fveq2d 
 |-  ( w = W -> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg m ) ` ( f oF ( dist ` w ) g ) ) = ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg m ) ` ( f oF ( dist ` W ) g ) ) )
13 7 7 12 mpoeq123dv 
 |-  ( w = W -> ( 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 ) ) ) )
14 oveq2 
 |-  ( m = M -> ( W sitg m ) = ( W sitg M ) )
15 14 dmeqd 
 |-  ( m = M -> dom ( W sitg m ) = dom ( W sitg M ) )
16 oveq2 
 |-  ( m = M -> ( ( RR*s |`s ( 0 [,] +oo ) ) sitg m ) = ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) )
17 1 eqcomi 
 |-  ( dist ` W ) = D
18 ofeq 
 |-  ( ( dist ` W ) = D -> oF ( dist ` W ) = oF D )
19 17 18 mp1i 
 |-  ( m = M -> oF ( dist ` W ) = oF D )
20 19 oveqd 
 |-  ( m = M -> ( f oF ( dist ` W ) g ) = ( f oF D g ) )
21 16 20 fveq12d 
 |-  ( m = M -> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg m ) ` ( f oF ( dist ` W ) g ) ) = ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF D g ) ) )
22 15 15 21 mpoeq123dv 
 |-  ( m = 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 ) ) ) = ( f e. dom ( W sitg M ) , g e. dom ( W sitg M ) |-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF D g ) ) ) )
23 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 ) ) ) )
24 ovex 
 |-  ( W sitg M ) e. _V
25 24 dmex 
 |-  dom ( W sitg M ) e. _V
26 25 25 mpoex 
 |-  ( f e. dom ( W sitg M ) , g e. dom ( W sitg M ) |-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF D g ) ) ) e. _V
27 13 22 23 26 ovmpo 
 |-  ( ( W e. _V /\ M e. U. ran measures ) -> ( W sitm M ) = ( f e. dom ( W sitg M ) , g e. dom ( W sitg M ) |-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF D g ) ) ) )
28 5 3 27 syl2anc 
 |-  ( 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 D g ) ) ) )