This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐹 ∈ 𝑄 → 𝐹 : 𝐵 ⟶ 𝐵 )