Metamath Proof Explorer


Theorem evls1rhm

Description: Polynomial evaluation is a homomorphism (into the product ring). (Contributed by AV, 11-Sep-2019)

Ref Expression
Hypotheses evls1rhm.q
|- Q = ( S evalSub1 R )
evls1rhm.b
|- B = ( Base ` S )
evls1rhm.t
|- T = ( S ^s B )
evls1rhm.u
|- U = ( S |`s R )
evls1rhm.w
|- W = ( Poly1 ` U )
Assertion evls1rhm
|- ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom T ) )

Proof

Step Hyp Ref Expression
1 evls1rhm.q
 |-  Q = ( S evalSub1 R )
2 evls1rhm.b
 |-  B = ( Base ` S )
3 evls1rhm.t
 |-  T = ( S ^s B )
4 evls1rhm.u
 |-  U = ( S |`s R )
5 evls1rhm.w
 |-  W = ( Poly1 ` U )
6 2 subrgss
 |-  ( R e. ( SubRing ` S ) -> R C_ B )
7 6 adantl
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> R C_ B )
8 elpwg
 |-  ( R e. ( SubRing ` S ) -> ( R e. ~P B <-> R C_ B ) )
9 8 adantl
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( R e. ~P B <-> R C_ B ) )
10 7 9 mpbird
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> R e. ~P B )
11 eqid
 |-  ( 1o evalSub S ) = ( 1o evalSub S )
12 1 11 2 evls1fval
 |-  ( ( S e. CRing /\ R e. ~P B ) -> Q = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub S ) ` R ) ) )
13 10 12 syldan
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> Q = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub S ) ` R ) ) )
14 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 } ) ) ) )
15 2 3 14 evls1rhmlem
 |-  ( S e. CRing -> ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) e. ( ( S ^s ( B ^m 1o ) ) RingHom T ) )
16 1on
 |-  1o e. On
17 eqid
 |-  ( ( 1o evalSub S ) ` R ) = ( ( 1o evalSub S ) ` R )
18 eqid
 |-  ( 1o mPoly U ) = ( 1o mPoly U )
19 eqid
 |-  ( S ^s ( B ^m 1o ) ) = ( S ^s ( B ^m 1o ) )
20 17 18 4 19 2 evlsrhm
 |-  ( ( 1o e. On /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( 1o evalSub S ) ` R ) e. ( ( 1o mPoly U ) RingHom ( S ^s ( B ^m 1o ) ) ) )
21 16 20 mp3an1
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( 1o evalSub S ) ` R ) e. ( ( 1o mPoly U ) RingHom ( S ^s ( B ^m 1o ) ) ) )
22 eqidd
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( Base ` W ) = ( Base ` W ) )
23 eqidd
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( Base ` ( S ^s ( B ^m 1o ) ) ) = ( Base ` ( S ^s ( B ^m 1o ) ) ) )
24 eqid
 |-  ( PwSer1 ` U ) = ( PwSer1 ` U )
25 eqid
 |-  ( Base ` W ) = ( Base ` W )
26 5 24 25 ply1bas
 |-  ( Base ` W ) = ( Base ` ( 1o mPoly U ) )
27 26 a1i
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( Base ` W ) = ( Base ` ( 1o mPoly U ) ) )
28 eqid
 |-  ( +g ` W ) = ( +g ` W )
29 5 18 28 ply1plusg
 |-  ( +g ` W ) = ( +g ` ( 1o mPoly U ) )
30 29 a1i
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( +g ` W ) = ( +g ` ( 1o mPoly U ) ) )
31 30 oveqdr
 |-  ( ( ( S e. CRing /\ R e. ( SubRing ` S ) ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( x ( +g ` W ) y ) = ( x ( +g ` ( 1o mPoly U ) ) y ) )
32 eqidd
 |-  ( ( ( S e. CRing /\ R e. ( SubRing ` S ) ) /\ ( x e. ( Base ` ( S ^s ( B ^m 1o ) ) ) /\ y e. ( Base ` ( S ^s ( B ^m 1o ) ) ) ) ) -> ( x ( +g ` ( S ^s ( B ^m 1o ) ) ) y ) = ( x ( +g ` ( S ^s ( B ^m 1o ) ) ) y ) )
33 eqid
 |-  ( .r ` W ) = ( .r ` W )
34 5 18 33 ply1mulr
 |-  ( .r ` W ) = ( .r ` ( 1o mPoly U ) )
35 34 a1i
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( .r ` W ) = ( .r ` ( 1o mPoly U ) ) )
36 35 oveqdr
 |-  ( ( ( S e. CRing /\ R e. ( SubRing ` S ) ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( x ( .r ` W ) y ) = ( x ( .r ` ( 1o mPoly U ) ) y ) )
37 eqidd
 |-  ( ( ( S e. CRing /\ R e. ( SubRing ` S ) ) /\ ( x e. ( Base ` ( S ^s ( B ^m 1o ) ) ) /\ y e. ( Base ` ( S ^s ( B ^m 1o ) ) ) ) ) -> ( x ( .r ` ( S ^s ( B ^m 1o ) ) ) y ) = ( x ( .r ` ( S ^s ( B ^m 1o ) ) ) y ) )
38 22 23 27 23 31 32 36 37 rhmpropd
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( W RingHom ( S ^s ( B ^m 1o ) ) ) = ( ( 1o mPoly U ) RingHom ( S ^s ( B ^m 1o ) ) ) )
39 21 38 eleqtrrd
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( 1o evalSub S ) ` R ) e. ( W RingHom ( S ^s ( B ^m 1o ) ) ) )
40 rhmco
 |-  ( ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) e. ( ( S ^s ( B ^m 1o ) ) RingHom T ) /\ ( ( 1o evalSub S ) ` R ) e. ( W RingHom ( S ^s ( B ^m 1o ) ) ) ) -> ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub S ) ` R ) ) e. ( W RingHom T ) )
41 15 39 40 syl2an2r
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub S ) ` R ) ) e. ( W RingHom T ) )
42 13 41 eqeltrd
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom T ) )