Theorem pf1f

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

	Ref	Expression
Hypotheses	pf1rcl.q	⊢ 𝑄 = ran ( eval1 ‘ 𝑅 )
	pf1f.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	pf1f	⊢ ( 𝐹 ∈ 𝑄 → 𝐹 : 𝐵 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		pf1rcl.q	⊢ 𝑄 = ran ( eval1 ‘ 𝑅 )
2		pf1f.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		eqid	⊢ ( 𝑅 ↑s 𝐵 ) = ( 𝑅 ↑s 𝐵 )
4		eqid	⊢ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐵 ) )
5	1	pf1rcl	⊢ ( 𝐹 ∈ 𝑄 → 𝑅 ∈ CRing )
6	2	fvexi	⊢ 𝐵 ∈ V
7	6	a1i	⊢ ( 𝐹 ∈ 𝑄 → 𝐵 ∈ V )
8	2 1	pf1subrg	⊢ ( 𝑅 ∈ CRing → 𝑄 ∈ ( SubRing ‘ ( 𝑅 ↑s 𝐵 ) ) )
9	4	subrgss	⊢ ( 𝑄 ∈ ( SubRing ‘ ( 𝑅 ↑s 𝐵 ) ) → 𝑄 ⊆ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
10	5 8 9	3syl	⊢ ( 𝐹 ∈ 𝑄 → 𝑄 ⊆ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
11		id	⊢ ( 𝐹 ∈ 𝑄 → 𝐹 ∈ 𝑄 )
12	10 11	sseldd	⊢ ( 𝐹 ∈ 𝑄 → 𝐹 ∈ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
13	3 2 4 5 7 12	pwselbas	⊢ ( 𝐹 ∈ 𝑄 → 𝐹 : 𝐵 ⟶ 𝐵 )