This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 |`s R )
evlsrhm.t 
|- T = ( S ^s ( B ^m I ) )
evlsrhm.b 
|- B = ( Base ` S )
Assertion evlsrhm 
|- ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( 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 |`s R )
4 evlsrhm.t 
 |-  T = ( S ^s ( B ^m I ) )
5 evlsrhm.b 
 |-  B = ( Base ` S )
6 eqid 
 |-  ( I mVar U ) = ( I mVar U )
7 eqid 
 |-  ( algSc ` W ) = ( algSc ` W )
8 eqid 
 |-  ( x e. R |-> ( ( B ^m I ) X. { x } ) ) = ( x e. R |-> ( ( B ^m I ) X. { x } ) )
9 eqid 
 |-  ( x e. I |-> ( y e. ( B ^m I ) |-> ( y ` x ) ) ) = ( x e. I |-> ( y e. ( B ^m I ) |-> ( y ` x ) ) )
10 1 2 6 3 4 5 7 8 9 evlsval2 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( Q e. ( W RingHom T ) /\ ( ( Q o. ( algSc ` W ) ) = ( x e. R |-> ( ( B ^m I ) X. { x } ) ) /\ ( Q o. ( I mVar U ) ) = ( x e. I |-> ( y e. ( B ^m I ) |-> ( y ` x ) ) ) ) ) )
11 10 simpld 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom T ) )