Metamath Proof Explorer

Theorem evlrhm

Description: The simple evaluation map is a ring homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses evlval.q ⊢ Q = I eval R
evlval.b ⊢ B = Base R
evlrhm.w ⊢ W = I mPoly R
evlrhm.t ⊢ T = R ↑ 𝑠 B I
Assertion evlrhm ⊢ I ∈ V ∧ R ∈ CRing → Q ∈ W RingHom T

Proof

Step Hyp Ref Expression
1 evlval.q ⊢ Q = I eval R
2 evlval.b ⊢ B = Base R
3 evlrhm.w ⊢ W = I mPoly R
4 evlrhm.t ⊢ T = R ↑ 𝑠 B I
5 crngring ⊢ R ∈ CRing → R ∈ Ring
6 5 adantl ⊢ I ∈ V ∧ R ∈ CRing → R ∈ Ring
7 2 subrgid ⊢ R ∈ Ring → B ∈ SubRing ⁡ R
8 6 7 syl ⊢ I ∈ V ∧ R ∈ CRing → B ∈ SubRing ⁡ R
9 1 2 evlval ⊢ Q = I evalSub R ⁡ B
10 eqid ⊢ I mPoly R ↾ 𝑠 B = I mPoly R ↾ 𝑠 B
11 eqid ⊢ R ↾ 𝑠 B = R ↾ 𝑠 B
12 9 10 11 4 2 evlsrhm ⊢ I ∈ V ∧ R ∈ CRing ∧ B ∈ SubRing ⁡ R → Q ∈ I mPoly R ↾ 𝑠 B RingHom T
13 8 12 mpd3an3 ⊢ I ∈ V ∧ R ∈ CRing → Q ∈ I mPoly R ↾ 𝑠 B RingHom T
14 2 ressid ⊢ R ∈ CRing → R ↾ 𝑠 B = R
15 14 adantl ⊢ I ∈ V ∧ R ∈ CRing → R ↾ 𝑠 B = R
16 15 oveq2d ⊢ I ∈ V ∧ R ∈ CRing → I mPoly R ↾ 𝑠 B = I mPoly R
17 16 3 eqtr4di ⊢ I ∈ V ∧ R ∈ CRing → I mPoly R ↾ 𝑠 B = W
18 17 oveq1d ⊢ I ∈ V ∧ R ∈ CRing → I mPoly R ↾ 𝑠 B RingHom T = W RingHom T
19 13 18 eleqtrd ⊢ I ∈ V ∧ R ∈ CRing → Q ∈ W RingHom T