This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem plyreres

Description: Real-coefficient polynomials restrict to real functions. (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Assertion plyreres 
|- ( F e. ( Poly ` RR ) -> ( F |` RR ) : RR --> RR )

Proof

Step Hyp Ref Expression
1 plybss 
 |-  ( F e. ( Poly ` RR ) -> RR C_ CC )
2 plyf 
 |-  ( F e. ( Poly ` RR ) -> F : CC --> CC )
3 ffn 
 |-  ( F : CC --> CC -> F Fn CC )
4 fnssresb 
 |-  ( F Fn CC -> ( ( F |` RR ) Fn RR <-> RR C_ CC ) )
5 2 3 4 3syl 
 |-  ( F e. ( Poly ` RR ) -> ( ( F |` RR ) Fn RR <-> RR C_ CC ) )
6 1 5 mpbird 
 |-  ( F e. ( Poly ` RR ) -> ( F |` RR ) Fn RR )
7 fvres 
 |-  ( a e. RR -> ( ( F |` RR ) ` a ) = ( F ` a ) )
8 7 adantl 
 |-  ( ( F e. ( Poly ` RR ) /\ a e. RR ) -> ( ( F |` RR ) ` a ) = ( F ` a ) )
9 recn 
 |-  ( a e. RR -> a e. CC )
10 ffvelcdm 
 |-  ( ( F : CC --> CC /\ a e. CC ) -> ( F ` a ) e. CC )
11 2 9 10 syl2an 
 |-  ( ( F e. ( Poly ` RR ) /\ a e. RR ) -> ( F ` a ) e. CC )
12 plyrecj 
 |-  ( ( F e. ( Poly ` RR ) /\ a e. CC ) -> ( * ` ( F ` a ) ) = ( F ` ( * ` a ) ) )
13 9 12 sylan2 
 |-  ( ( F e. ( Poly ` RR ) /\ a e. RR ) -> ( * ` ( F ` a ) ) = ( F ` ( * ` a ) ) )
14 cjre 
 |-  ( a e. RR -> ( * ` a ) = a )
15 14 adantl 
 |-  ( ( F e. ( Poly ` RR ) /\ a e. RR ) -> ( * ` a ) = a )
16 15 fveq2d 
 |-  ( ( F e. ( Poly ` RR ) /\ a e. RR ) -> ( F ` ( * ` a ) ) = ( F ` a ) )
17 13 16 eqtrd 
 |-  ( ( F e. ( Poly ` RR ) /\ a e. RR ) -> ( * ` ( F ` a ) ) = ( F ` a ) )
18 11 17 cjrebd 
 |-  ( ( F e. ( Poly ` RR ) /\ a e. RR ) -> ( F ` a ) e. RR )
19 8 18 eqeltrd 
 |-  ( ( F e. ( Poly ` RR ) /\ a e. RR ) -> ( ( F |` RR ) ` a ) e. RR )
20 19 ralrimiva 
 |-  ( F e. ( Poly ` RR ) -> A. a e. RR ( ( F |` RR ) ` a ) e. RR )
21 fnfvrnss 
 |-  ( ( ( F |` RR ) Fn RR /\ A. a e. RR ( ( F |` RR ) ` a ) e. RR ) -> ran ( F |` RR ) C_ RR )
22 6 20 21 syl2anc 
 |-  ( F e. ( Poly ` RR ) -> ran ( F |` RR ) C_ RR )
23 df-f 
 |-  ( ( F |` RR ) : RR --> RR <-> ( ( F |` RR ) Fn RR /\ ran ( F |` RR ) C_ RR ) )
24 6 22 23 sylanbrc 
 |-  ( F e. ( Poly ` RR ) -> ( F |` RR ) : RR --> RR )