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 syl5eq
 |-  ( ( 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 ) ) ) )