Metamath Proof Explorer


Theorem evlsrhm

Description: Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Stefan O'Rear, 12-Mar-2015)

Ref Expression
Hypotheses evlsrhm.q Q = I evalSub S R
evlsrhm.w W = I mPoly U
evlsrhm.u U = S 𝑠 R
evlsrhm.t T = S 𝑠 B I
evlsrhm.b B = Base S
Assertion evlsrhm I V S CRing R SubRing S Q W RingHom T

Proof

Step Hyp Ref Expression
1 evlsrhm.q Q = I evalSub S R
2 evlsrhm.w W = I mPoly U
3 evlsrhm.u U = S 𝑠 R
4 evlsrhm.t T = S 𝑠 B I
5 evlsrhm.b B = Base S
6 eqid I mVar U = I mVar U
7 eqid algSc W = algSc W
8 eqid x R B I × x = x R B I × x
9 eqid x I y B I y x = x I y B I y x
10 1 2 6 3 4 5 7 8 9 evlsval2 I V S CRing R SubRing S Q W RingHom T Q algSc W = x R B I × x Q I mVar U = x I y B I y x
11 10 simpld I V S CRing R SubRing S Q W RingHom T