Metamath Proof Explorer

Theorem ovolfs2

Description: Alternative expression for the interval length function. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypothesis ovolfs2.1 
|- G = ( ( abs o. - ) o. F )
Assertion ovolfs2 
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> G = ( ( vol* o. (,) ) o. F ) )

Proof

Step Hyp Ref Expression
1 ovolfs2.1 
 |-  G = ( ( abs o. - ) o. F )
2 ovolfcl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR /\ ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) )
3 ovolioo 
 |-  ( ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR /\ ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) -> ( vol* ` ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) ) = ( ( 2nd ` ( F ` n ) ) - ( 1st ` ( F ` n ) ) ) )
4 2 3 syl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( vol* ` ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) ) = ( ( 2nd ` ( F ` n ) ) - ( 1st ` ( F ` n ) ) ) )
5 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
6 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
7 5 6 sstri 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
8 ffvelrn 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( F ` n ) e. ( <_ i^i ( RR X. RR ) ) )
9 7 8 sselid 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( F ` n ) e. ( RR* X. RR* ) )
10 1st2nd2 
 |-  ( ( F ` n ) e. ( RR* X. RR* ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
11 9 10 syl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
12 11 fveq2d 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( (,) ` ( F ` n ) ) = ( (,) ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. ) )
13 df-ov 
 |-  ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) = ( (,) ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
14 12 13 eqtr4di 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( (,) ` ( F ` n ) ) = ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) )
15 14 fveq2d 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( vol* ` ( (,) ` ( F ` n ) ) ) = ( vol* ` ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) ) )
16 1 ovolfsval 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( G ` n ) = ( ( 2nd ` ( F ` n ) ) - ( 1st ` ( F ` n ) ) ) )
17 4 15 16 3eqtr4rd 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( G ` n ) = ( vol* ` ( (,) ` ( F ` n ) ) ) )
18 17 mpteq2dva 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( n e. NN |-> ( G ` n ) ) = ( n e. NN |-> ( vol* ` ( (,) ` ( F ` n ) ) ) ) )
19 1 ovolfsf 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> G : NN --> ( 0 [,) +oo ) )
20 19 feqmptd 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> G = ( n e. NN |-> ( G ` n ) ) )
21 id 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
22 21 feqmptd 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> F = ( n e. NN |-> ( F ` n ) ) )
23 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
24 23 a1i 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> (,) : ( RR* X. RR* ) --> ~P RR )
25 24 ffvelrnda 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. ( RR* X. RR* ) ) -> ( (,) ` x ) e. ~P RR )
26 24 feqmptd 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> (,) = ( x e. ( RR* X. RR* ) |-> ( (,) ` x ) ) )
27 ovolf 
 |-  vol* : ~P RR --> ( 0 [,] +oo )
28 27 a1i 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> vol* : ~P RR --> ( 0 [,] +oo ) )
29 28 feqmptd 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> vol* = ( y e. ~P RR |-> ( vol* ` y ) ) )
30 fveq2 
 |-  ( y = ( (,) ` x ) -> ( vol* ` y ) = ( vol* ` ( (,) ` x ) ) )
31 25 26 29 30 fmptco 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( vol* o. (,) ) = ( x e. ( RR* X. RR* ) |-> ( vol* ` ( (,) ` x ) ) ) )
32 2fveq3 
 |-  ( x = ( F ` n ) -> ( vol* ` ( (,) ` x ) ) = ( vol* ` ( (,) ` ( F ` n ) ) ) )
33 9 22 31 32 fmptco 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( vol* o. (,) ) o. F ) = ( n e. NN |-> ( vol* ` ( (,) ` ( F ` n ) ) ) ) )
34 18 20 33 3eqtr4d 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> G = ( ( vol* o. (,) ) o. F ) )