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 ( 𝐹 ∈ ( 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 ‘ ℝ ) → ( 𝐹 ↾ ℝ ) : ℝ ⟶ ℝ )