Metamath Proof Explorer


Theorem mpfsubrg

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

Ref Expression
Hypothesis mpfsubrg.q Q = ran I evalSub S R
Assertion mpfsubrg I V S CRing R SubRing S Q SubRing S 𝑠 Base S I

Proof

Step Hyp Ref Expression
1 mpfsubrg.q Q = ran I evalSub S R
2 eqid I evalSub S R = I evalSub S R
3 eqid I mPoly S 𝑠 R = I mPoly S 𝑠 R
4 eqid S 𝑠 R = S 𝑠 R
5 eqid S 𝑠 Base S I = S 𝑠 Base S I
6 eqid Base S = Base S
7 2 3 4 5 6 evlsrhm I V S CRing R SubRing S I evalSub S R I mPoly S 𝑠 R RingHom S 𝑠 Base S I
8 eqid Base I mPoly S 𝑠 R = Base I mPoly S 𝑠 R
9 eqid Base S 𝑠 Base S I = Base S 𝑠 Base S I
10 8 9 rhmf I evalSub S R I mPoly S 𝑠 R RingHom S 𝑠 Base S I I evalSub S R : Base I mPoly S 𝑠 R Base S 𝑠 Base S I
11 ffn I evalSub S R : Base I mPoly S 𝑠 R Base S 𝑠 Base S I I evalSub S R Fn Base I mPoly S 𝑠 R
12 fnima I evalSub S R Fn Base I mPoly S 𝑠 R I evalSub S R Base I mPoly S 𝑠 R = ran I evalSub S R
13 11 12 syl I evalSub S R : Base I mPoly S 𝑠 R Base S 𝑠 Base S I I evalSub S R Base I mPoly S 𝑠 R = ran I evalSub S R
14 7 10 13 3syl I V S CRing R SubRing S I evalSub S R Base I mPoly S 𝑠 R = ran I evalSub S R
15 1 14 eqtr4id I V S CRing R SubRing S Q = I evalSub S R Base I mPoly S 𝑠 R
16 4 subrgring R SubRing S S 𝑠 R Ring
17 3 mplring I V S 𝑠 R Ring I mPoly S 𝑠 R Ring
18 16 17 sylan2 I V R SubRing S I mPoly S 𝑠 R Ring
19 18 3adant2 I V S CRing R SubRing S I mPoly S 𝑠 R Ring
20 8 subrgid I mPoly S 𝑠 R Ring Base I mPoly S 𝑠 R SubRing I mPoly S 𝑠 R
21 19 20 syl I V S CRing R SubRing S Base I mPoly S 𝑠 R SubRing I mPoly S 𝑠 R
22 rhmima I evalSub S R I mPoly S 𝑠 R RingHom S 𝑠 Base S I Base I mPoly S 𝑠 R SubRing I mPoly S 𝑠 R I evalSub S R Base I mPoly S 𝑠 R SubRing S 𝑠 Base S I
23 7 21 22 syl2anc I V S CRing R SubRing S I evalSub S R Base I mPoly S 𝑠 R SubRing S 𝑠 Base S I
24 15 23 eqeltrd I V S CRing R SubRing S Q SubRing S 𝑠 Base S I