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 8 ofeqd 
 |-  ( w = W -> oF ( dist ` w ) = oF ( dist ` W ) )
10 9 oveqd 
 |-  ( w = W -> ( f oF ( dist ` w ) g ) = ( f oF ( dist ` W ) g ) )
11 10 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 ) ) )
12 7 7 11 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 ) ) ) )
13 oveq2 
 |-  ( m = M -> ( W sitg m ) = ( W sitg M ) )
14 13 dmeqd 
 |-  ( m = M -> dom ( W sitg m ) = dom ( W sitg M ) )
15 oveq2 
 |-  ( m = M -> ( ( RR*s |`s ( 0 [,] +oo ) ) sitg m ) = ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) )
16 1 eqcomi 
 |-  ( dist ` W ) = D
17 ofeq 
 |-  ( ( dist ` W ) = D -> oF ( dist ` W ) = oF D )
18 16 17 mp1i 
 |-  ( m = M -> oF ( dist ` W ) = oF D )
19 18 oveqd 
 |-  ( m = M -> ( f oF ( dist ` W ) g ) = ( f oF D g ) )
20 15 19 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 ) ) )
21 14 14 20 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 ) ) ) )
22 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 ) ) ) )
23 ovex 
 |-  ( W sitg M ) e. _V
24 23 dmex 
 |-  dom ( W sitg M ) e. _V
25 24 24 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
26 12 21 22 25 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 ) ) ) )
27 5 3 26 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 ) ) ) )