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 )