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 ) ) ) ) ) )