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

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 
 |-  ( Base ` P ) = ( Base ` P )
17 2 16 ply1bas 
 |-  ( Base ` P ) = ( Base ` ( 1o mPoly R ) )
18 17 a1i 
 |-  ( R e. CRing -> ( Base ` P ) = ( Base ` ( 1o mPoly R ) ) )
19 eqid 
 |-  ( +g ` P ) = ( +g ` P )
20 2 10 19 ply1plusg 
 |-  ( +g ` P ) = ( +g ` ( 1o mPoly R ) )
21 20 a1i 
 |-  ( R e. CRing -> ( +g ` P ) = ( +g ` ( 1o mPoly R ) ) )
22 21 oveqdr 
 |-  ( ( R e. CRing /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( x ( +g ` P ) y ) = ( x ( +g ` ( 1o mPoly R ) ) y ) )
23 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 ) )
24 eqid 
 |-  ( .r ` P ) = ( .r ` P )
25 2 10 24 ply1mulr 
 |-  ( .r ` P ) = ( .r ` ( 1o mPoly R ) )
26 25 a1i 
 |-  ( R e. CRing -> ( .r ` P ) = ( .r ` ( 1o mPoly R ) ) )
27 26 oveqdr 
 |-  ( ( R e. CRing /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( x ( .r ` P ) y ) = ( x ( .r ` ( 1o mPoly R ) ) y ) )
28 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 ) )
29 14 15 18 15 22 23 27 28 rhmpropd 
 |-  ( R e. CRing -> ( P RingHom ( R ^s ( B ^m 1o ) ) ) = ( ( 1o mPoly R ) RingHom ( R ^s ( B ^m 1o ) ) ) )
30 13 29 eleqtrrd 
 |-  ( R e. CRing -> ( 1o eval R ) e. ( P RingHom ( R ^s ( B ^m 1o ) ) ) )
31 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 ) )
32 8 30 31 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 ) )
33 6 32 eqeltrid 
 |-  ( R e. CRing -> O e. ( P RingHom T ) )