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