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 ^s ( B ^m I ) )
Assertion evlrhm 
|- ( ( I e. V /\ R e. CRing ) -> Q e. ( 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 ^s ( B ^m I ) )
5 crngring 
 |-  ( R e. CRing -> R e. Ring )
6 5 adantl 
 |-  ( ( I e. V /\ R e. CRing ) -> R e. Ring )
7 2 subrgid 
 |-  ( R e. Ring -> B e. ( SubRing ` R ) )
8 6 7 syl 
 |-  ( ( I e. V /\ R e. CRing ) -> B e. ( SubRing ` R ) )
9 1 2 evlval 
 |-  Q = ( ( I evalSub R ) ` B )
10 eqid 
 |-  ( I mPoly ( R |`s B ) ) = ( I mPoly ( R |`s B ) )
11 eqid 
 |-  ( R |`s B ) = ( R |`s B )
12 9 10 11 4 2 evlsrhm 
 |-  ( ( I e. V /\ R e. CRing /\ B e. ( SubRing ` R ) ) -> Q e. ( ( I mPoly ( R |`s B ) ) RingHom T ) )
13 8 12 mpd3an3 
 |-  ( ( I e. V /\ R e. CRing ) -> Q e. ( ( I mPoly ( R |`s B ) ) RingHom T ) )
14 2 ressid 
 |-  ( R e. CRing -> ( R |`s B ) = R )
15 14 adantl 
 |-  ( ( I e. V /\ R e. CRing ) -> ( R |`s B ) = R )
16 15 oveq2d 
 |-  ( ( I e. V /\ R e. CRing ) -> ( I mPoly ( R |`s B ) ) = ( I mPoly R ) )
17 16 3 eqtr4di 
 |-  ( ( I e. V /\ R e. CRing ) -> ( I mPoly ( R |`s B ) ) = W )
18 17 oveq1d 
 |-  ( ( I e. V /\ R e. CRing ) -> ( ( I mPoly ( R |`s B ) ) RingHom T ) = ( W RingHom T ) )
19 13 18 eleqtrd 
 |-  ( ( I e. V /\ R e. CRing ) -> Q e. ( W RingHom T ) )