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