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 ) )