| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ply1annidl.o |
|- O = ( R evalSub1 S ) |
| 2 |
|
ply1annidl.p |
|- P = ( Poly1 ` ( R |`s S ) ) |
| 3 |
|
ply1annidl.b |
|- B = ( Base ` R ) |
| 4 |
|
ply1annidl.r |
|- ( ph -> R e. CRing ) |
| 5 |
|
ply1annidl.s |
|- ( ph -> S e. ( SubRing ` R ) ) |
| 6 |
|
ply1annidl.a |
|- ( ph -> A e. B ) |
| 7 |
|
ply1annidl.0 |
|- .0. = ( 0g ` R ) |
| 8 |
|
ply1annidl.q |
|- Q = { q e. dom O | ( ( O ` q ) ` A ) = .0. } |
| 9 |
|
eqid |
|- ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) = ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) |
| 10 |
1 2 3 4 5 6 7 8 9
|
ply1annidllem |
|- ( ph -> Q = ( `' ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) " { .0. } ) ) |
| 11 |
|
eqid |
|- ( Base ` P ) = ( Base ` P ) |
| 12 |
1 2 3 11 4 5 6 9
|
evls1maprhm |
|- ( ph -> ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) e. ( P RingHom R ) ) |
| 13 |
4
|
crngringd |
|- ( ph -> R e. Ring ) |
| 14 |
|
eqid |
|- ( LIdeal ` R ) = ( LIdeal ` R ) |
| 15 |
14 7
|
lidl0 |
|- ( R e. Ring -> { .0. } e. ( LIdeal ` R ) ) |
| 16 |
13 15
|
syl |
|- ( ph -> { .0. } e. ( LIdeal ` R ) ) |
| 17 |
|
eqid |
|- ( LIdeal ` P ) = ( LIdeal ` P ) |
| 18 |
17
|
rhmpreimaidl |
|- ( ( ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) e. ( P RingHom R ) /\ { .0. } e. ( LIdeal ` R ) ) -> ( `' ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) " { .0. } ) e. ( LIdeal ` P ) ) |
| 19 |
12 16 18
|
syl2anc |
|- ( ph -> ( `' ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) " { .0. } ) e. ( LIdeal ` P ) ) |
| 20 |
10 19
|
eqeltrd |
|- ( ph -> Q e. ( LIdeal ` P ) ) |