This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mon1puc1p

Description: Monic polynomials are unitic. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses mon1puc1p.c 
|- C = ( Unic1p ` R )
mon1puc1p.m 
|- M = ( Monic1p ` R )
Assertion mon1puc1p 
|- ( ( R e. Ring /\ X e. M ) -> X e. C )

Proof

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 )