Theorem plyrecld

Description: Closure of a polynomial with real coefficients. (Contributed by Thierry Arnoux, 18-Sep-2018)

	Ref	Expression
Hypotheses	plyrecld.1	|- ( ph -> F e. ( Poly ` RR ) )
	plyrecld.2	|- ( ph -> X e. RR )
Assertion	plyrecld	|- ( ph -> ( F ` X ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		plyrecld.1	|- ( ph -> F e. ( Poly ` RR ) )
2		plyrecld.2	|- ( ph -> X e. RR )
3		fvres	|- ( X e. RR -> ( ( F |` RR ) ` X ) = ( F ` X ) )
4	2 3	syl	|- ( ph -> ( ( F |` RR ) ` X ) = ( F ` X ) )
5		plyreres	|- ( F e. ( Poly ` RR ) -> ( F |` RR ) : RR --> RR )
6	1 5	syl	|- ( ph -> ( F |` RR ) : RR --> RR )
7	6 2	ffvelrnd	|- ( ph -> ( ( F |` RR ) ` X ) e. RR )
8	4 7	eqeltrrd	|- ( ph -> ( F ` X ) e. RR )