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 ∈ Poly ⁡ ℝ → F ↾ ℝ : ℝ ⟶ ℝ

Proof

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