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 7 10 11 12 4syl ⊢ I ∈ V ∧ S ∈ CRing ∧ R ∈ SubRing ⁡ S → I evalSub S ⁡ R Base I mPoly S ↾ 𝑠 R = ran ⁡ I evalSub S ⁡ R
14 1 13 eqtr4id ⊢ I ∈ V ∧ S ∈ CRing ∧ R ∈ SubRing ⁡ S → Q = I evalSub S ⁡ R Base I mPoly S ↾ 𝑠 R
15 4 subrgring ⊢ R ∈ SubRing ⁡ S → S ↾ 𝑠 R ∈ Ring
16 3 mplring ⊢ I ∈ V ∧ S ↾ 𝑠 R ∈ Ring → I mPoly S ↾ 𝑠 R ∈ Ring
17 15 16 sylan2 ⊢ I ∈ V ∧ R ∈ SubRing ⁡ S → I mPoly S ↾ 𝑠 R ∈ Ring
18 17 3adant2 ⊢ I ∈ V ∧ S ∈ CRing ∧ R ∈ SubRing ⁡ S → I mPoly S ↾ 𝑠 R ∈ Ring
19 8 subrgid ⊢ I mPoly S ↾ 𝑠 R ∈ Ring → Base I mPoly S ↾ 𝑠 R ∈ SubRing ⁡ I mPoly S ↾ 𝑠 R
20 18 19 syl ⊢ I ∈ V ∧ S ∈ CRing ∧ R ∈ SubRing ⁡ S → Base I mPoly S ↾ 𝑠 R ∈ SubRing ⁡ I mPoly S ↾ 𝑠 R
21 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
22 7 20 21 syl2anc ⊢ I ∈ V ∧ S ∈ CRing ∧ R ∈ SubRing ⁡ S → I evalSub S ⁡ R Base I mPoly S ↾ 𝑠 R ∈ SubRing ⁡ S ↑ 𝑠 Base S I
23 14 22 eqeltrd ⊢ I ∈ V ∧ S ∈ CRing ∧ R ∈ SubRing ⁡ S → Q ∈ SubRing ⁡ S ↑ 𝑠 Base S I