Metamath Proof Explorer


Theorem pf1subrg

Description: Polynomial functions are a subring. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses pf1const.b B = Base R
pf1const.q Q = ran eval 1 R
Assertion pf1subrg R CRing Q SubRing R 𝑠 B

Proof

Step Hyp Ref Expression
1 pf1const.b B = Base R
2 pf1const.q Q = ran eval 1 R
3 eqid eval 1 R = eval 1 R
4 eqid Poly 1 R = Poly 1 R
5 eqid R 𝑠 B = R 𝑠 B
6 3 4 5 1 evl1rhm R CRing eval 1 R Poly 1 R RingHom R 𝑠 B
7 eqid Base Poly 1 R = Base Poly 1 R
8 eqid Base R 𝑠 B = Base R 𝑠 B
9 7 8 rhmf eval 1 R Poly 1 R RingHom R 𝑠 B eval 1 R : Base Poly 1 R Base R 𝑠 B
10 ffn eval 1 R : Base Poly 1 R Base R 𝑠 B eval 1 R Fn Base Poly 1 R
11 fnima eval 1 R Fn Base Poly 1 R eval 1 R Base Poly 1 R = ran eval 1 R
12 6 9 10 11 4syl R CRing eval 1 R Base Poly 1 R = ran eval 1 R
13 12 2 eqtr4di R CRing eval 1 R Base Poly 1 R = Q
14 4 ply1assa R CRing Poly 1 R AssAlg
15 assaring Poly 1 R AssAlg Poly 1 R Ring
16 7 subrgid Poly 1 R Ring Base Poly 1 R SubRing Poly 1 R
17 14 15 16 3syl R CRing Base Poly 1 R SubRing Poly 1 R
18 rhmima eval 1 R Poly 1 R RingHom R 𝑠 B Base Poly 1 R SubRing Poly 1 R eval 1 R Base Poly 1 R SubRing R 𝑠 B
19 6 17 18 syl2anc R CRing eval 1 R Base Poly 1 R SubRing R 𝑠 B
20 13 19 eqeltrrd R CRing Q SubRing R 𝑠 B