This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem volicofmpt

Description: ( ( vol o. [,) ) o. F ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses volicofmpt.1 
|- F/_ x F
volicofmpt.2 
|- ( ph -> F : A --> ( RR X. RR* ) )
Assertion volicofmpt 
|- ( ph -> ( ( vol o. [,) ) o. F ) = ( x e. A |-> ( vol ` ( ( 1st ` ( F ` x ) ) [,) ( 2nd ` ( F ` x ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 volicofmpt.1 
 |-  F/_ x F
2 volicofmpt.2 
 |-  ( ph -> F : A --> ( RR X. RR* ) )
3 nfcv 
 |-  F/_ x A
4 nfcv 
 |-  F/_ x ( vol o. [,) )
5 4 1 nfco 
 |-  F/_ x ( ( vol o. [,) ) o. F )
6 2 volicoff 
 |-  ( ph -> ( ( vol o. [,) ) o. F ) : A --> ( 0 [,] +oo ) )
7 3 5 6 feqmptdf 
 |-  ( ph -> ( ( vol o. [,) ) o. F ) = ( x e. A |-> ( ( ( vol o. [,) ) o. F ) ` x ) ) )
8 ressxr 
 |-  RR C_ RR*
9 xpss1 
 |-  ( RR C_ RR* -> ( RR X. RR* ) C_ ( RR* X. RR* ) )
10 8 9 ax-mp 
 |-  ( RR X. RR* ) C_ ( RR* X. RR* )
11 10 a1i 
 |-  ( ph -> ( RR X. RR* ) C_ ( RR* X. RR* ) )
12 2 11 fssd 
 |-  ( ph -> F : A --> ( RR* X. RR* ) )
13 12 adantr 
 |-  ( ( ph /\ x e. A ) -> F : A --> ( RR* X. RR* ) )
14 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
15 13 14 fvvolicof 
 |-  ( ( ph /\ x e. A ) -> ( ( ( vol o. [,) ) o. F ) ` x ) = ( vol ` ( ( 1st ` ( F ` x ) ) [,) ( 2nd ` ( F ` x ) ) ) ) )
16 15 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( ( ( vol o. [,) ) o. F ) ` x ) ) = ( x e. A |-> ( vol ` ( ( 1st ` ( F ` x ) ) [,) ( 2nd ` ( F ` x ) ) ) ) ) )
17 7 16 eqtrd 
 |-  ( ph -> ( ( vol o. [,) ) o. F ) = ( x e. A |-> ( vol ` ( ( 1st ` ( F ` x ) ) [,) ( 2nd ` ( F ` x ) ) ) ) ) )