Metamath Proof Explorer

Theorem ovolfsval

Description: The value of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Hypothesis ovolfs.1 
|- G = ( ( abs o. - ) o. F )
Assertion ovolfsval 
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( G ` N ) = ( ( 2nd ` ( F ` N ) ) - ( 1st ` ( F ` N ) ) ) )

Proof

Step Hyp Ref Expression
1 ovolfs.1 
 |-  G = ( ( abs o. - ) o. F )
2 1 fveq1i 
 |-  ( G ` N ) = ( ( ( abs o. - ) o. F ) ` N )
3 fvco3 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( ( ( abs o. - ) o. F ) ` N ) = ( ( abs o. - ) ` ( F ` N ) ) )
4 2 3 eqtrid 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( G ` N ) = ( ( abs o. - ) ` ( F ` N ) ) )
5 ffvelrn 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( F ` N ) e. ( <_ i^i ( RR X. RR ) ) )
6 5 elin2d 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( F ` N ) e. ( RR X. RR ) )
7 1st2nd2 
 |-  ( ( F ` N ) e. ( RR X. RR ) -> ( F ` N ) = <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. )
8 6 7 syl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( F ` N ) = <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. )
9 8 fveq2d 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( ( abs o. - ) ` ( F ` N ) ) = ( ( abs o. - ) ` <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. ) )
10 df-ov 
 |-  ( ( 1st ` ( F ` N ) ) ( abs o. - ) ( 2nd ` ( F ` N ) ) ) = ( ( abs o. - ) ` <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. )
11 9 10 eqtr4di 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( ( abs o. - ) ` ( F ` N ) ) = ( ( 1st ` ( F ` N ) ) ( abs o. - ) ( 2nd ` ( F ` N ) ) ) )
12 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 ) ) ) )
13 12 simp1d 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( 1st ` ( F ` N ) ) e. RR )
14 13 recnd 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( 1st ` ( F ` N ) ) e. CC )
15 12 simp2d 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( 2nd ` ( F ` N ) ) e. RR )
16 15 recnd 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( 2nd ` ( F ` N ) ) e. CC )
17 eqid 
 |-  ( abs o. - ) = ( abs o. - )
18 17 cnmetdval 
 |-  ( ( ( 1st ` ( F ` N ) ) e. CC /\ ( 2nd ` ( F ` N ) ) e. CC ) -> ( ( 1st ` ( F ` N ) ) ( abs o. - ) ( 2nd ` ( F ` N ) ) ) = ( abs ` ( ( 1st ` ( F ` N ) ) - ( 2nd ` ( F ` N ) ) ) ) )
19 14 16 18 syl2anc 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( ( 1st ` ( F ` N ) ) ( abs o. - ) ( 2nd ` ( F ` N ) ) ) = ( abs ` ( ( 1st ` ( F ` N ) ) - ( 2nd ` ( F ` N ) ) ) ) )
20 abssuble0 
 |-  ( ( ( 1st ` ( F ` N ) ) e. RR /\ ( 2nd ` ( F ` N ) ) e. RR /\ ( 1st ` ( F ` N ) ) <_ ( 2nd ` ( F ` N ) ) ) -> ( abs ` ( ( 1st ` ( F ` N ) ) - ( 2nd ` ( F ` N ) ) ) ) = ( ( 2nd ` ( F ` N ) ) - ( 1st ` ( F ` N ) ) ) )
21 12 20 syl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( abs ` ( ( 1st ` ( F ` N ) ) - ( 2nd ` ( F ` N ) ) ) ) = ( ( 2nd ` ( F ` N ) ) - ( 1st ` ( F ` N ) ) ) )
22 19 21 eqtrd 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( ( 1st ` ( F ` N ) ) ( abs o. - ) ( 2nd ` ( F ` N ) ) ) = ( ( 2nd ` ( F ` N ) ) - ( 1st ` ( F ` N ) ) ) )
23 11 22 eqtrd 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( ( abs o. - ) ` ( F ` N ) ) = ( ( 2nd ` ( F ` N ) ) - ( 1st ` ( F ` N ) ) ) )
24 4 23 eqtrd 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( G ` N ) = ( ( 2nd ` ( F ` N ) ) - ( 1st ` ( F ` N ) ) ) )