Metamath Proof Explorer

Theorem fvvolicof

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

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

Proof

Step Hyp Ref Expression
1 fvvolicof.f 
 |-  ( ph -> F : A --> ( RR* X. RR* ) )
2 fvvolicof.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 icof 
 |-  [,) : ( 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 ) ) ) ) )