Metamath Proof Explorer

Theorem fvvolioof

Description: The function value of the Lebesgue measure of an open interval composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021)

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

Proof

Step Hyp Ref Expression
1 fvvolioof.f 
 |-  ( ph -> F : A --> ( RR* X. RR* ) )
2 fvvolioof.x 
 |-  ( ph -> X e. A )
3 1 ffund 
 |-  ( ph -> Fun F )
4 1 fdmd 
 |-  ( ph -> dom F = A )
5 4 eqcomd 
 |-  ( ph -> A = dom F )
6 2 5 eleqtrd 
 |-  ( ph -> X e. dom F )
7 fvco 
 |-  ( ( Fun F /\ X e. dom F ) -> ( ( ( vol o. (,) ) o. F ) ` X ) = ( ( vol o. (,) ) ` ( F ` X ) ) )
8 3 6 7 syl2anc 
 |-  ( ph -> ( ( ( vol o. (,) ) o. F ) ` X ) = ( ( vol o. (,) ) ` ( F ` X ) ) )
9 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
10 ffun 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> Fun (,) )
11 9 10 ax-mp 
 |-  Fun (,)
12 11 a1i 
 |-  ( ph -> Fun (,) )
13 1 2 ffvelrnd 
 |-  ( ph -> ( F ` X ) e. ( RR* X. RR* ) )
14 9 fdmi 
 |-  dom (,) = ( RR* X. RR* )
15 13 14 eleqtrrdi 
 |-  ( ph -> ( F ` X ) e. dom (,) )
16 fvco 
 |-  ( ( Fun (,) /\ ( F ` X ) e. dom (,) ) -> ( ( vol o. (,) ) ` ( F ` X ) ) = ( vol ` ( (,) ` ( F ` X ) ) ) )
17 12 15 16 syl2anc 
 |-  ( ph -> ( ( vol o. (,) ) ` ( F ` X ) ) = ( vol ` ( (,) ` ( F ` X ) ) ) )
18 df-ov 
 |-  ( ( 1st ` ( F ` X ) ) (,) ( 2nd ` ( F ` X ) ) ) = ( (,) ` <. ( 1st ` ( F ` X ) ) , ( 2nd ` ( F ` X ) ) >. )
19 18 a1i 
 |-  ( ph -> ( ( 1st ` ( F ` X ) ) (,) ( 2nd ` ( F ` X ) ) ) = ( (,) ` <. ( 1st ` ( F ` X ) ) , ( 2nd ` ( F ` X ) ) >. ) )
20 1st2nd2 
 |-  ( ( F ` X ) e. ( RR* X. RR* ) -> ( F ` X ) = <. ( 1st ` ( F ` X ) ) , ( 2nd ` ( F ` X ) ) >. )
21 13 20 syl 
 |-  ( ph -> ( F ` X ) = <. ( 1st ` ( F ` X ) ) , ( 2nd ` ( F ` X ) ) >. )
22 21 eqcomd 
 |-  ( ph -> <. ( 1st ` ( F ` X ) ) , ( 2nd ` ( F ` X ) ) >. = ( F ` X ) )
23 22 fveq2d 
 |-  ( ph -> ( (,) ` <. ( 1st ` ( F ` X ) ) , ( 2nd ` ( F ` X ) ) >. ) = ( (,) ` ( F ` X ) ) )
24 19 23 eqtr2d 
 |-  ( ph -> ( (,) ` ( F ` X ) ) = ( ( 1st ` ( F ` X ) ) (,) ( 2nd ` ( F ` X ) ) ) )
25 24 fveq2d 
 |-  ( ph -> ( vol ` ( (,) ` ( F ` X ) ) ) = ( vol ` ( ( 1st ` ( F ` X ) ) (,) ( 2nd ` ( F ` X ) ) ) ) )
26 8 17 25 3eqtrd 
 |-  ( ph -> ( ( ( vol o. (,) ) o. F ) ` X ) = ( vol ` ( ( 1st ` ( F ` X ) ) (,) ( 2nd ` ( F ` X ) ) ) ) )