Theorem plyreres

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

	Ref	Expression
Assertion	plyreres	⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝐹 ↾ ℝ ) : ℝ ⟶ ℝ )

Proof

Step	Hyp	Ref	Expression
1		plybss	⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ℝ ⊆ ℂ )
2		plyf	⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → 𝐹 : ℂ ⟶ ℂ )
3		ffn	⊢ ( 𝐹 : ℂ ⟶ ℂ → 𝐹 Fn ℂ )
4		fnssresb	⊢ ( 𝐹 Fn ℂ → ( ( 𝐹 ↾ ℝ ) Fn ℝ ↔ ℝ ⊆ ℂ ) )
5	2 3 4	3syl	⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( ( 𝐹 ↾ ℝ ) Fn ℝ ↔ ℝ ⊆ ℂ ) )
6	1 5	mpbird	⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝐹 ↾ ℝ ) Fn ℝ )
7		fvres	⊢ ( 𝑎 ∈ ℝ → ( ( 𝐹 ↾ ℝ ) ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 ) )
8	7	adantl	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑎 ∈ ℝ ) → ( ( 𝐹 ↾ ℝ ) ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 ) )
9		recn	⊢ ( 𝑎 ∈ ℝ → 𝑎 ∈ ℂ )
10		ffvelcdm	⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ 𝑎 ∈ ℂ ) → ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
11	2 9 10	syl2an	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑎 ∈ ℝ ) → ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
12		plyrecj	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑎 ∈ ℂ ) → ( ∗ ‘ ( 𝐹 ‘ 𝑎 ) ) = ( 𝐹 ‘ ( ∗ ‘ 𝑎 ) ) )
13	9 12	sylan2	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑎 ∈ ℝ ) → ( ∗ ‘ ( 𝐹 ‘ 𝑎 ) ) = ( 𝐹 ‘ ( ∗ ‘ 𝑎 ) ) )
14		cjre	⊢ ( 𝑎 ∈ ℝ → ( ∗ ‘ 𝑎 ) = 𝑎 )
15	14	adantl	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑎 ∈ ℝ ) → ( ∗ ‘ 𝑎 ) = 𝑎 )
16	15	fveq2d	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑎 ∈ ℝ ) → ( 𝐹 ‘ ( ∗ ‘ 𝑎 ) ) = ( 𝐹 ‘ 𝑎 ) )
17	13 16	eqtrd	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑎 ∈ ℝ ) → ( ∗ ‘ ( 𝐹 ‘ 𝑎 ) ) = ( 𝐹 ‘ 𝑎 ) )
18	11 17	cjrebd	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑎 ∈ ℝ ) → ( 𝐹 ‘ 𝑎 ) ∈ ℝ )
19	8 18	eqeltrd	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑎 ∈ ℝ ) → ( ( 𝐹 ↾ ℝ ) ‘ 𝑎 ) ∈ ℝ )
20	19	ralrimiva	⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ∀ 𝑎 ∈ ℝ ( ( 𝐹 ↾ ℝ ) ‘ 𝑎 ) ∈ ℝ )
21		fnfvrnss	⊢ ( ( ( 𝐹 ↾ ℝ ) Fn ℝ ∧ ∀ 𝑎 ∈ ℝ ( ( 𝐹 ↾ ℝ ) ‘ 𝑎 ) ∈ ℝ ) → ran ( 𝐹 ↾ ℝ ) ⊆ ℝ )
22	6 20 21	syl2anc	⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ran ( 𝐹 ↾ ℝ ) ⊆ ℝ )
23		df-f	⊢ ( ( 𝐹 ↾ ℝ ) : ℝ ⟶ ℝ ↔ ( ( 𝐹 ↾ ℝ ) Fn ℝ ∧ ran ( 𝐹 ↾ ℝ ) ⊆ ℝ ) )
24	6 22 23	sylanbrc	⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝐹 ↾ ℝ ) : ℝ ⟶ ℝ )