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 
 |-  ( Base ` W ) = ( Base ` W )
25 5 24 ply1bas 
 |-  ( Base ` W ) = ( Base ` ( 1o mPoly U ) )
26 25 a1i 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( Base ` W ) = ( Base ` ( 1o mPoly U ) ) )
27 eqid 
 |-  ( +g ` W ) = ( +g ` W )
28 5 18 27 ply1plusg 
 |-  ( +g ` W ) = ( +g ` ( 1o mPoly U ) )
29 28 a1i 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( +g ` W ) = ( +g ` ( 1o mPoly U ) ) )
30 29 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 ) )
31 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 ) )
32 eqid 
 |-  ( .r ` W ) = ( .r ` W )
33 5 18 32 ply1mulr 
 |-  ( .r ` W ) = ( .r ` ( 1o mPoly U ) )
34 33 a1i 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( .r ` W ) = ( .r ` ( 1o mPoly U ) ) )
35 34 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 ) )
36 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 ) )
37 22 23 26 23 30 31 35 36 rhmpropd 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( W RingHom ( S ^s ( B ^m 1o ) ) ) = ( ( 1o mPoly U ) RingHom ( S ^s ( B ^m 1o ) ) ) )
38 21 37 eleqtrrd 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( 1o evalSub S ) ` R ) e. ( W RingHom ( S ^s ( B ^m 1o ) ) ) )
39 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 ) )
40 15 38 39 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 ) )
41 13 40 eqeltrd 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom T ) )