Metamath Proof Explorer


Theorem ovolfsf

Description: Closure for the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Hypothesis ovolfs.1
|- G = ( ( abs o. - ) o. F )
Assertion ovolfsf
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> G : NN --> ( 0 [,) +oo ) )

Proof

Step Hyp Ref Expression
1 ovolfs.1
 |-  G = ( ( abs o. - ) o. F )
2 absf
 |-  abs : CC --> RR
3 subf
 |-  - : ( CC X. CC ) --> CC
4 fco
 |-  ( ( abs : CC --> RR /\ - : ( CC X. CC ) --> CC ) -> ( abs o. - ) : ( CC X. CC ) --> RR )
5 2 3 4 mp2an
 |-  ( abs o. - ) : ( CC X. CC ) --> RR
6 inss2
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
7 ax-resscn
 |-  RR C_ CC
8 xpss12
 |-  ( ( RR C_ CC /\ RR C_ CC ) -> ( RR X. RR ) C_ ( CC X. CC ) )
9 7 7 8 mp2an
 |-  ( RR X. RR ) C_ ( CC X. CC )
10 6 9 sstri
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( CC X. CC )
11 fss
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( CC X. CC ) ) -> F : NN --> ( CC X. CC ) )
12 10 11 mpan2
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> F : NN --> ( CC X. CC ) )
13 fco
 |-  ( ( ( abs o. - ) : ( CC X. CC ) --> RR /\ F : NN --> ( CC X. CC ) ) -> ( ( abs o. - ) o. F ) : NN --> RR )
14 5 12 13 sylancr
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. F ) : NN --> RR )
15 1 feq1i
 |-  ( G : NN --> RR <-> ( ( abs o. - ) o. F ) : NN --> RR )
16 14 15 sylibr
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> G : NN --> RR )
17 16 ffnd
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> G Fn NN )
18 16 ffvelrnda
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( G ` x ) e. RR )
19 ovolfcl
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( ( 1st ` ( F ` x ) ) e. RR /\ ( 2nd ` ( F ` x ) ) e. RR /\ ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) ) )
20 subge0
 |-  ( ( ( 2nd ` ( F ` x ) ) e. RR /\ ( 1st ` ( F ` x ) ) e. RR ) -> ( 0 <_ ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) <-> ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) ) )
21 20 ancoms
 |-  ( ( ( 1st ` ( F ` x ) ) e. RR /\ ( 2nd ` ( F ` x ) ) e. RR ) -> ( 0 <_ ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) <-> ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) ) )
22 21 biimp3ar
 |-  ( ( ( 1st ` ( F ` x ) ) e. RR /\ ( 2nd ` ( F ` x ) ) e. RR /\ ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) ) -> 0 <_ ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) )
23 19 22 syl
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> 0 <_ ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) )
24 1 ovolfsval
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( G ` x ) = ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) )
25 23 24 breqtrrd
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> 0 <_ ( G ` x ) )
26 elrege0
 |-  ( ( G ` x ) e. ( 0 [,) +oo ) <-> ( ( G ` x ) e. RR /\ 0 <_ ( G ` x ) ) )
27 18 25 26 sylanbrc
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( G ` x ) e. ( 0 [,) +oo ) )
28 27 ralrimiva
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> A. x e. NN ( G ` x ) e. ( 0 [,) +oo ) )
29 ffnfv
 |-  ( G : NN --> ( 0 [,) +oo ) <-> ( G Fn NN /\ A. x e. NN ( G ` x ) e. ( 0 [,) +oo ) ) )
30 17 28 29 sylanbrc
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> G : NN --> ( 0 [,) +oo ) )