Metamath Proof Explorer

Theorem evl1rhm

Description: Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Mario Carneiro, 12-Jun-2015) (Proof shortened by AV, 13-Sep-2019)

Ref Expression
Hypotheses evl1rhm.q 
|- O = ( eval1 ` R )
evl1rhm.w 
|- P = ( Poly1 ` R )
evl1rhm.t 
|- T = ( R ^s B )
evl1rhm.b 
|- B = ( Base ` R )
Assertion evl1rhm 
|- ( R e. CRing -> O e. ( P RingHom T ) )

Proof

Step Hyp Ref Expression
1 evl1rhm.q 
 |-  O = ( eval1 ` R )
2 evl1rhm.w 
 |-  P = ( Poly1 ` R )
3 evl1rhm.t 
 |-  T = ( R ^s B )
4 evl1rhm.b 
 |-  B = ( Base ` R )
5 eqid 
 |-  ( 1o eval R ) = ( 1o eval R )
6 1 5 4 evl1fval 
 |-  O = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval R ) )
7 eqid 
 |-  ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) = ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) )
8 4 3 7 evls1rhmlem 
 |-  ( R e. CRing -> ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) e. ( ( R ^s ( B ^m 1o ) ) RingHom T ) )
9 1on 
 |-  1o e. On
10 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
11 eqid 
 |-  ( R ^s ( B ^m 1o ) ) = ( R ^s ( B ^m 1o ) )
12 5 4 10 11 evlrhm 
 |-  ( ( 1o e. On /\ R e. CRing ) -> ( 1o eval R ) e. ( ( 1o mPoly R ) RingHom ( R ^s ( B ^m 1o ) ) ) )
13 9 12 mpan 
 |-  ( R e. CRing -> ( 1o eval R ) e. ( ( 1o mPoly R ) RingHom ( R ^s ( B ^m 1o ) ) ) )
14 eqidd 
 |-  ( R e. CRing -> ( Base ` P ) = ( Base ` P ) )
15 eqidd 
 |-  ( R e. CRing -> ( Base ` ( R ^s ( B ^m 1o ) ) ) = ( Base ` ( R ^s ( B ^m 1o ) ) ) )
16 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
17 eqid 
 |-  ( Base ` P ) = ( Base ` P )
18 2 16 17 ply1bas 
 |-  ( Base ` P ) = ( Base ` ( 1o mPoly R ) )
19 18 a1i 
 |-  ( R e. CRing -> ( Base ` P ) = ( Base ` ( 1o mPoly R ) ) )
20 eqid 
 |-  ( +g ` P ) = ( +g ` P )
21 2 10 20 ply1plusg 
 |-  ( +g ` P ) = ( +g ` ( 1o mPoly R ) )
22 21 a1i 
 |-  ( R e. CRing -> ( +g ` P ) = ( +g ` ( 1o mPoly R ) ) )
23 22 oveqdr 
 |-  ( ( R e. CRing /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( x ( +g ` P ) y ) = ( x ( +g ` ( 1o mPoly R ) ) y ) )
24 eqidd 
 |-  ( ( R e. CRing /\ ( x e. ( Base ` ( R ^s ( B ^m 1o ) ) ) /\ y e. ( Base ` ( R ^s ( B ^m 1o ) ) ) ) ) -> ( x ( +g ` ( R ^s ( B ^m 1o ) ) ) y ) = ( x ( +g ` ( R ^s ( B ^m 1o ) ) ) y ) )
25 eqid 
 |-  ( .r ` P ) = ( .r ` P )
26 2 10 25 ply1mulr 
 |-  ( .r ` P ) = ( .r ` ( 1o mPoly R ) )
27 26 a1i 
 |-  ( R e. CRing -> ( .r ` P ) = ( .r ` ( 1o mPoly R ) ) )
28 27 oveqdr 
 |-  ( ( R e. CRing /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( x ( .r ` P ) y ) = ( x ( .r ` ( 1o mPoly R ) ) y ) )
29 eqidd 
 |-  ( ( R e. CRing /\ ( x e. ( Base ` ( R ^s ( B ^m 1o ) ) ) /\ y e. ( Base ` ( R ^s ( B ^m 1o ) ) ) ) ) -> ( x ( .r ` ( R ^s ( B ^m 1o ) ) ) y ) = ( x ( .r ` ( R ^s ( B ^m 1o ) ) ) y ) )
30 14 15 19 15 23 24 28 29 rhmpropd 
 |-  ( R e. CRing -> ( P RingHom ( R ^s ( B ^m 1o ) ) ) = ( ( 1o mPoly R ) RingHom ( R ^s ( B ^m 1o ) ) ) )
31 13 30 eleqtrrd 
 |-  ( R e. CRing -> ( 1o eval R ) e. ( P RingHom ( R ^s ( B ^m 1o ) ) ) )
32 rhmco 
 |-  ( ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) e. ( ( R ^s ( B ^m 1o ) ) RingHom T ) /\ ( 1o eval R ) e. ( P RingHom ( R ^s ( B ^m 1o ) ) ) ) -> ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval R ) ) e. ( P RingHom T ) )
33 8 31 32 syl2anc 
 |-  ( R e. CRing -> ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval R ) ) e. ( P RingHom T ) )
34 6 33 eqeltrid 
 |-  ( R e. CRing -> O e. ( P RingHom T ) )