Step |
Hyp |
Ref |
Expression |
1 |
|
mon1puc1p.c |
|- C = ( Unic1p ` R ) |
2 |
|
mon1puc1p.m |
|- M = ( Monic1p ` R ) |
3 |
|
eqid |
|- ( Poly1 ` R ) = ( Poly1 ` R ) |
4 |
|
eqid |
|- ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) ) |
5 |
3 4 2
|
mon1pcl |
|- ( X e. M -> X e. ( Base ` ( Poly1 ` R ) ) ) |
6 |
5
|
adantl |
|- ( ( R e. Ring /\ X e. M ) -> X e. ( Base ` ( Poly1 ` R ) ) ) |
7 |
|
eqid |
|- ( 0g ` ( Poly1 ` R ) ) = ( 0g ` ( Poly1 ` R ) ) |
8 |
3 7 2
|
mon1pn0 |
|- ( X e. M -> X =/= ( 0g ` ( Poly1 ` R ) ) ) |
9 |
8
|
adantl |
|- ( ( R e. Ring /\ X e. M ) -> X =/= ( 0g ` ( Poly1 ` R ) ) ) |
10 |
|
eqid |
|- ( deg1 ` R ) = ( deg1 ` R ) |
11 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
12 |
10 11 2
|
mon1pldg |
|- ( X e. M -> ( ( coe1 ` X ) ` ( ( deg1 ` R ) ` X ) ) = ( 1r ` R ) ) |
13 |
12
|
adantl |
|- ( ( R e. Ring /\ X e. M ) -> ( ( coe1 ` X ) ` ( ( deg1 ` R ) ` X ) ) = ( 1r ` R ) ) |
14 |
|
eqid |
|- ( Unit ` R ) = ( Unit ` R ) |
15 |
14 11
|
1unit |
|- ( R e. Ring -> ( 1r ` R ) e. ( Unit ` R ) ) |
16 |
15
|
adantr |
|- ( ( R e. Ring /\ X e. M ) -> ( 1r ` R ) e. ( Unit ` R ) ) |
17 |
13 16
|
eqeltrd |
|- ( ( R e. Ring /\ X e. M ) -> ( ( coe1 ` X ) ` ( ( deg1 ` R ) ` X ) ) e. ( Unit ` R ) ) |
18 |
3 4 7 10 1 14
|
isuc1p |
|- ( X e. C <-> ( X e. ( Base ` ( Poly1 ` R ) ) /\ X =/= ( 0g ` ( Poly1 ` R ) ) /\ ( ( coe1 ` X ) ` ( ( deg1 ` R ) ` X ) ) e. ( Unit ` R ) ) ) |
19 |
6 9 17 18
|
syl3anbrc |
|- ( ( R e. Ring /\ X e. M ) -> X e. C ) |