plyreres

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

		Ref	Expression
	Assertion	plyreres	$⊢ F \in Poly (ℝ) \to ({F ↾}_{ℝ}) : ℝ ⟶ ℝ$

Proof

Step	Hyp	Ref	Expression
1		plybss	$⊢ F \in Poly (ℝ) \to ℝ \subseteq ℂ$
2		plyf	$⊢ F \in Poly (ℝ) \to F : ℂ ⟶ ℂ$
3		ffn	$⊢ F : ℂ ⟶ ℂ \to F Fn ℂ$
4		fnssresb	$⊢ F Fn ℂ \to (({F ↾}_{ℝ}) Fn ℝ \leftrightarrow ℝ \subseteq ℂ)$
5	2 3 4	3syl	$⊢ F \in Poly (ℝ) \to (({F ↾}_{ℝ}) Fn ℝ \leftrightarrow ℝ \subseteq ℂ)$
6	1 5	mpbird	$⊢ F \in Poly (ℝ) \to ({F ↾}_{ℝ}) Fn ℝ$
7		fvres	$⊢ a \in ℝ \to ({F ↾}_{ℝ}) (a) = F (a)$
8	7	adantl	$⊢ (F \in Poly (ℝ) \land a \in ℝ) \to ({F ↾}_{ℝ}) (a) = F (a)$
9		recn	$⊢ a \in ℝ \to a \in ℂ$
10		ffvelcdm	$⊢ (F : ℂ ⟶ ℂ \land a \in ℂ) \to F (a) \in ℂ$
11	2 9 10	syl2an	$⊢ (F \in Poly (ℝ) \land a \in ℝ) \to F (a) \in ℂ$
12		plyrecj	$⊢ (F \in Poly (ℝ) \land a \in ℂ) \to \overline{F (a)} = F (\overline{a})$
13	9 12	sylan2	$⊢ (F \in Poly (ℝ) \land a \in ℝ) \to \overline{F (a)} = F (\overline{a})$
14		cjre	$⊢ a \in ℝ \to \overline{a} = a$
15	14	adantl	$⊢ (F \in Poly (ℝ) \land a \in ℝ) \to \overline{a} = a$
16	15	fveq2d	$⊢ (F \in Poly (ℝ) \land a \in ℝ) \to F (\overline{a}) = F (a)$
17	13 16	eqtrd	$⊢ (F \in Poly (ℝ) \land a \in ℝ) \to \overline{F (a)} = F (a)$
18	11 17	cjrebd	$⊢ (F \in Poly (ℝ) \land a \in ℝ) \to F (a) \in ℝ$
19	8 18	eqeltrd	$⊢ (F \in Poly (ℝ) \land a \in ℝ) \to ({F ↾}_{ℝ}) (a) \in ℝ$
20	19	ralrimiva	$⊢ F \in Poly (ℝ) \to \forall a \in ℝ ({F ↾}_{ℝ}) (a) \in ℝ$
21		fnfvrnss	$⊢ (({F ↾}_{ℝ}) Fn ℝ \land \forall a \in ℝ ({F ↾}_{ℝ}) (a) \in ℝ) \to ran ({F ↾}_{ℝ}) \subseteq ℝ$
22	6 20 21	syl2anc	$⊢ F \in Poly (ℝ) \to ran ({F ↾}_{ℝ}) \subseteq ℝ$
23		df-f	$⊢ ({F ↾}_{ℝ}) : ℝ ⟶ ℝ \leftrightarrow (({F ↾}_{ℝ}) Fn ℝ \land ran ({F ↾}_{ℝ}) \subseteq ℝ)$
24	6 22 23	sylanbrc	$⊢ F \in Poly (ℝ) \to ({F ↾}_{ℝ}) : ℝ ⟶ ℝ$

Metamath Proof Explorer

Theorem plyreres

Proof