pf1f

Description: Polynomial functions are functions. (Contributed by Mario Carneiro, 12-Jun-2015)

Step	Hyp	Ref	Expression
1		pf1rcl.q	$⊢ Q = ran {eval}_{1} (R)$
2		pf1f.b	$⊢ B = {Base}_{R}$
3		eqid	$⊢ R ↑_{𝑠} B = R ↑_{𝑠} B$
4		eqid	$⊢ {Base}_{(R ↑_{𝑠} B)} = {Base}_{(R ↑_{𝑠} B)}$
5	1	pf1rcl	$⊢ F \in Q \to R \in CRing$
6	2	fvexi	$⊢ B \in V$
7	6	a1i	$⊢ F \in Q \to B \in V$
8	2 1	pf1subrg	$⊢ R \in CRing \to Q \in SubRing (R ↑_{𝑠} B)$
9	4	subrgss	$⊢ Q \in SubRing (R ↑_{𝑠} B) \to Q \subseteq {Base}_{(R ↑_{𝑠} B)}$
10	5 8 9	3syl	$⊢ F \in Q \to Q \subseteq {Base}_{(R ↑_{𝑠} B)}$
11		id	$⊢ F \in Q \to F \in Q$
12	10 11	sseldd	$⊢ F \in Q \to F \in {Base}_{(R ↑_{𝑠} B)}$
13	3 2 4 5 7 12	pwselbas	$⊢ F \in Q \to F : B ⟶ B$

Metamath Proof Explorer