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