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