Metamath Proof Explorer

Theorem voliooicof

Description: The Lebesgue measure of open intervals is the same as the Lebesgue measure of left-closed right-open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypothesis voliooicof.1 
|- ( ph -> F : A --> ( RR X. RR ) )
Assertion voliooicof 
|- ( ph -> ( ( vol o. (,) ) o. F ) = ( ( vol o. [,) ) o. F ) )

Proof

Step Hyp Ref Expression
1 voliooicof.1 
 |-  ( ph -> F : A --> ( RR X. RR ) )
2 volioof 
 |-  ( vol o. (,) ) : ( RR* X. RR* ) --> ( 0 [,] +oo )
3 2 a1i 
 |-  ( ph -> ( vol o. (,) ) : ( RR* X. RR* ) --> ( 0 [,] +oo ) )
4 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
5 4 a1i 
 |-  ( ph -> ( RR X. RR ) C_ ( RR* X. RR* ) )
6 3 5 1 fcoss 
 |-  ( ph -> ( ( vol o. (,) ) o. F ) : A --> ( 0 [,] +oo ) )
7 6 ffnd 
 |-  ( ph -> ( ( vol o. (,) ) o. F ) Fn A )
8 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
9 8 a1i 
 |-  ( ph -> vol : dom vol --> ( 0 [,] +oo ) )
10 icof 
 |-  [,) : ( RR* X. RR* ) --> ~P RR*
11 10 a1i 
 |-  ( ph -> [,) : ( RR* X. RR* ) --> ~P RR* )
12 11 5 1 fcoss 
 |-  ( ph -> ( [,) o. F ) : A --> ~P RR* )
13 12 ffnd 
 |-  ( ph -> ( [,) o. F ) Fn A )
14 1 adantr 
 |-  ( ( ph /\ x e. A ) -> F : A --> ( RR X. RR ) )
15 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
16 14 15 fvovco 
 |-  ( ( ph /\ x e. A ) -> ( ( [,) o. F ) ` x ) = ( ( 1st ` ( F ` x ) ) [,) ( 2nd ` ( F ` x ) ) ) )
17 1 ffvelcdmda 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. ( RR X. RR ) )
18 xp1st 
 |-  ( ( F ` x ) e. ( RR X. RR ) -> ( 1st ` ( F ` x ) ) e. RR )
19 17 18 syl 
 |-  ( ( ph /\ x e. A ) -> ( 1st ` ( F ` x ) ) e. RR )
20 xp2nd 
 |-  ( ( F ` x ) e. ( RR X. RR ) -> ( 2nd ` ( F ` x ) ) e. RR )
21 17 20 syl 
 |-  ( ( ph /\ x e. A ) -> ( 2nd ` ( F ` x ) ) e. RR )
22 21 rexrd 
 |-  ( ( ph /\ x e. A ) -> ( 2nd ` ( F ` x ) ) e. RR* )
23 icombl 
 |-  ( ( ( 1st ` ( F ` x ) ) e. RR /\ ( 2nd ` ( F ` x ) ) e. RR* ) -> ( ( 1st ` ( F ` x ) ) [,) ( 2nd ` ( F ` x ) ) ) e. dom vol )
24 19 22 23 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( ( 1st ` ( F ` x ) ) [,) ( 2nd ` ( F ` x ) ) ) e. dom vol )
25 16 24 eqeltrd 
 |-  ( ( ph /\ x e. A ) -> ( ( [,) o. F ) ` x ) e. dom vol )
26 25 ralrimiva 
 |-  ( ph -> A. x e. A ( ( [,) o. F ) ` x ) e. dom vol )
27 13 26 jca 
 |-  ( ph -> ( ( [,) o. F ) Fn A /\ A. x e. A ( ( [,) o. F ) ` x ) e. dom vol ) )
28 ffnfv 
 |-  ( ( [,) o. F ) : A --> dom vol <-> ( ( [,) o. F ) Fn A /\ A. x e. A ( ( [,) o. F ) ` x ) e. dom vol ) )
29 27 28 sylibr 
 |-  ( ph -> ( [,) o. F ) : A --> dom vol )
30 fco 
 |-  ( ( vol : dom vol --> ( 0 [,] +oo ) /\ ( [,) o. F ) : A --> dom vol ) -> ( vol o. ( [,) o. F ) ) : A --> ( 0 [,] +oo ) )
31 9 29 30 syl2anc 
 |-  ( ph -> ( vol o. ( [,) o. F ) ) : A --> ( 0 [,] +oo ) )
32 coass 
 |-  ( ( vol o. [,) ) o. F ) = ( vol o. ( [,) o. F ) )
33 32 a1i 
 |-  ( ph -> ( ( vol o. [,) ) o. F ) = ( vol o. ( [,) o. F ) ) )
34 33 feq1d 
 |-  ( ph -> ( ( ( vol o. [,) ) o. F ) : A --> ( 0 [,] +oo ) <-> ( vol o. ( [,) o. F ) ) : A --> ( 0 [,] +oo ) ) )
35 31 34 mpbird 
 |-  ( ph -> ( ( vol o. [,) ) o. F ) : A --> ( 0 [,] +oo ) )
36 35 ffnd 
 |-  ( ph -> ( ( vol o. [,) ) o. F ) Fn A )
37 19 21 voliooico 
 |-  ( ( ph /\ x e. A ) -> ( vol ` ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) ) = ( vol ` ( ( 1st ` ( F ` x ) ) [,) ( 2nd ` ( F ` x ) ) ) ) )
38 1 5 fssd 
 |-  ( ph -> F : A --> ( RR* X. RR* ) )
39 38 adantr 
 |-  ( ( ph /\ x e. A ) -> F : A --> ( RR* X. RR* ) )
40 39 15 fvvolioof 
 |-  ( ( ph /\ x e. A ) -> ( ( ( vol o. (,) ) o. F ) ` x ) = ( vol ` ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) ) )
41 39 15 fvvolicof 
 |-  ( ( ph /\ x e. A ) -> ( ( ( vol o. [,) ) o. F ) ` x ) = ( vol ` ( ( 1st ` ( F ` x ) ) [,) ( 2nd ` ( F ` x ) ) ) ) )
42 37 40 41 3eqtr4d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( vol o. (,) ) o. F ) ` x ) = ( ( ( vol o. [,) ) o. F ) ` x ) )
43 7 36 42 eqfnfvd 
 |-  ( ph -> ( ( vol o. (,) ) o. F ) = ( ( vol o. [,) ) o. F ) )