Step |
Hyp |
Ref |
Expression |
1 |
|
rhmply1.p |
|- P = ( Poly1 ` R ) |
2 |
|
rhmply1.q |
|- Q = ( Poly1 ` S ) |
3 |
|
rhmply1.b |
|- B = ( Base ` P ) |
4 |
|
rhmply1.f |
|- F = ( p e. B |-> ( H o. p ) ) |
5 |
|
rhmply1.h |
|- ( ph -> H e. ( R RingHom S ) ) |
6 |
|
eqid |
|- ( 1o mPoly R ) = ( 1o mPoly R ) |
7 |
|
eqid |
|- ( 1o mPoly S ) = ( 1o mPoly S ) |
8 |
1 3
|
ply1bas |
|- B = ( Base ` ( 1o mPoly R ) ) |
9 |
|
1oex |
|- 1o e. _V |
10 |
9
|
a1i |
|- ( ph -> 1o e. _V ) |
11 |
6 7 8 4 10 5
|
rhmmpl |
|- ( ph -> F e. ( ( 1o mPoly R ) RingHom ( 1o mPoly S ) ) ) |
12 |
3
|
a1i |
|- ( ph -> B = ( Base ` P ) ) |
13 |
|
eqid |
|- ( Base ` Q ) = ( Base ` Q ) |
14 |
13
|
a1i |
|- ( ph -> ( Base ` Q ) = ( Base ` Q ) ) |
15 |
8
|
a1i |
|- ( ph -> B = ( Base ` ( 1o mPoly R ) ) ) |
16 |
2 13
|
ply1bas |
|- ( Base ` Q ) = ( Base ` ( 1o mPoly S ) ) |
17 |
16
|
a1i |
|- ( ph -> ( Base ` Q ) = ( Base ` ( 1o mPoly S ) ) ) |
18 |
|
eqid |
|- ( +g ` P ) = ( +g ` P ) |
19 |
1 6 18
|
ply1plusg |
|- ( +g ` P ) = ( +g ` ( 1o mPoly R ) ) |
20 |
19
|
oveqi |
|- ( x ( +g ` P ) y ) = ( x ( +g ` ( 1o mPoly R ) ) y ) |
21 |
20
|
a1i |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` P ) y ) = ( x ( +g ` ( 1o mPoly R ) ) y ) ) |
22 |
|
eqid |
|- ( +g ` Q ) = ( +g ` Q ) |
23 |
2 7 22
|
ply1plusg |
|- ( +g ` Q ) = ( +g ` ( 1o mPoly S ) ) |
24 |
23
|
oveqi |
|- ( x ( +g ` Q ) y ) = ( x ( +g ` ( 1o mPoly S ) ) y ) |
25 |
24
|
a1i |
|- ( ( ph /\ ( x e. ( Base ` Q ) /\ y e. ( Base ` Q ) ) ) -> ( x ( +g ` Q ) y ) = ( x ( +g ` ( 1o mPoly S ) ) y ) ) |
26 |
|
eqid |
|- ( .r ` P ) = ( .r ` P ) |
27 |
1 6 26
|
ply1mulr |
|- ( .r ` P ) = ( .r ` ( 1o mPoly R ) ) |
28 |
27
|
oveqi |
|- ( x ( .r ` P ) y ) = ( x ( .r ` ( 1o mPoly R ) ) y ) |
29 |
28
|
a1i |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` P ) y ) = ( x ( .r ` ( 1o mPoly R ) ) y ) ) |
30 |
|
eqid |
|- ( .r ` Q ) = ( .r ` Q ) |
31 |
2 7 30
|
ply1mulr |
|- ( .r ` Q ) = ( .r ` ( 1o mPoly S ) ) |
32 |
31
|
oveqi |
|- ( x ( .r ` Q ) y ) = ( x ( .r ` ( 1o mPoly S ) ) y ) |
33 |
32
|
a1i |
|- ( ( ph /\ ( x e. ( Base ` Q ) /\ y e. ( Base ` Q ) ) ) -> ( x ( .r ` Q ) y ) = ( x ( .r ` ( 1o mPoly S ) ) y ) ) |
34 |
12 14 15 17 21 25 29 33
|
rhmpropd |
|- ( ph -> ( P RingHom Q ) = ( ( 1o mPoly R ) RingHom ( 1o mPoly S ) ) ) |
35 |
11 34
|
eleqtrrd |
|- ( ph -> F e. ( P RingHom Q ) ) |