Metamath Proof Explorer

Theorem volioofmpt

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

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

Proof

Step Hyp Ref Expression
1 volioofmpt.x 
 |-  F/_ x F
2 volioofmpt.f 
 |-  ( 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 volioof 
 |-  ( vol o. (,) ) : ( RR* X. RR* ) --> ( 0 [,] +oo )
7 6 a1i 
 |-  ( ph -> ( vol o. (,) ) : ( RR* X. RR* ) --> ( 0 [,] +oo ) )
8 fco 
 |-  ( ( ( vol o. (,) ) : ( RR* X. RR* ) --> ( 0 [,] +oo ) /\ F : A --> ( RR* X. RR* ) ) -> ( ( vol o. (,) ) o. F ) : A --> ( 0 [,] +oo ) )
9 7 2 8 syl2anc 
 |-  ( ph -> ( ( vol o. (,) ) o. F ) : A --> ( 0 [,] +oo ) )
10 3 5 9 feqmptdf 
 |-  ( ph -> ( ( vol o. (,) ) o. F ) = ( x e. A |-> ( ( ( vol o. (,) ) o. F ) ` x ) ) )
11 2 adantr 
 |-  ( ( ph /\ x e. A ) -> F : A --> ( RR* X. RR* ) )
12 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
13 11 12 fvvolioof 
 |-  ( ( ph /\ x e. A ) -> ( ( ( vol o. (,) ) o. F ) ` x ) = ( vol ` ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) ) )
14 13 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( ( ( vol o. (,) ) o. F ) ` x ) ) = ( x e. A |-> ( vol ` ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) ) ) )
15 10 14 eqtrd 
 |-  ( ph -> ( ( vol o. (,) ) o. F ) = ( x e. A |-> ( vol ` ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) ) ) )