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=IevalSubSR
evlsrhm.w W=ImPolyU
evlsrhm.u U=S𝑠R
evlsrhm.t T=S𝑠BI
evlsrhm.b B=BaseS
Assertion evlsrhm IVSCRingRSubRingSQWRingHomT

Proof

Step Hyp Ref Expression
1 evlsrhm.q Q=IevalSubSR
2 evlsrhm.w W=ImPolyU
3 evlsrhm.u U=S𝑠R
4 evlsrhm.t T=S𝑠BI
5 evlsrhm.b B=BaseS
6 eqid ImVarU=ImVarU
7 eqid algScW=algScW
8 eqid xRBI×x=xRBI×x
9 eqid xIyBIyx=xIyBIyx
10 1 2 6 3 4 5 7 8 9 evlsval2 IVSCRingRSubRingSQWRingHomTQalgScW=xRBI×xQImVarU=xIyBIyx
11 10 simpld IVSCRingRSubRingSQWRingHomT