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