Metamath Proof Explorer

Theorem drnguc1p

Description: Over a division ring, all nonzero polynomials are unitic. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses drnguc1p.p 
|- P = ( Poly1 ` R )
drnguc1p.b 
|- B = ( Base ` P )
drnguc1p.z 
|- .0. = ( 0g ` P )
drnguc1p.c 
|- C = ( Unic1p ` R )
Assertion drnguc1p 
|- ( ( R e. DivRing /\ F e. B /\ F =/= .0. ) -> F e. C )

Proof

Step Hyp Ref Expression
1 drnguc1p.p 
 |-  P = ( Poly1 ` R )
2 drnguc1p.b 
 |-  B = ( Base ` P )
3 drnguc1p.z 
 |-  .0. = ( 0g ` P )
4 drnguc1p.c 
 |-  C = ( Unic1p ` R )
5 simp2 
 |-  ( ( R e. DivRing /\ F e. B /\ F =/= .0. ) -> F e. B )
6 simp3 
 |-  ( ( R e. DivRing /\ F e. B /\ F =/= .0. ) -> F =/= .0. )
7 eqid 
 |-  ( coe1 ` F ) = ( coe1 ` F )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 7 2 1 8 coe1f 
 |-  ( F e. B -> ( coe1 ` F ) : NN0 --> ( Base ` R ) )
10 9 3ad2ant2 
 |-  ( ( R e. DivRing /\ F e. B /\ F =/= .0. ) -> ( coe1 ` F ) : NN0 --> ( Base ` R ) )
11 drngring 
 |-  ( R e. DivRing -> R e. Ring )
12 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
13 12 1 3 2 deg1nn0cl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( ( deg1 ` R ) ` F ) e. NN0 )
14 11 13 syl3an1 
 |-  ( ( R e. DivRing /\ F e. B /\ F =/= .0. ) -> ( ( deg1 ` R ) ` F ) e. NN0 )
15 10 14 ffvelrnd 
 |-  ( ( R e. DivRing /\ F e. B /\ F =/= .0. ) -> ( ( coe1 ` F ) ` ( ( deg1 ` R ) ` F ) ) e. ( Base ` R ) )
16 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
17 12 1 3 2 16 7 deg1ldg 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( ( coe1 ` F ) ` ( ( deg1 ` R ) ` F ) ) =/= ( 0g ` R ) )
18 11 17 syl3an1 
 |-  ( ( R e. DivRing /\ F e. B /\ F =/= .0. ) -> ( ( coe1 ` F ) ` ( ( deg1 ` R ) ` F ) ) =/= ( 0g ` R ) )
19 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
20 8 19 16 drngunit 
 |-  ( R e. DivRing -> ( ( ( coe1 ` F ) ` ( ( deg1 ` R ) ` F ) ) e. ( Unit ` R ) <-> ( ( ( coe1 ` F ) ` ( ( deg1 ` R ) ` F ) ) e. ( Base ` R ) /\ ( ( coe1 ` F ) ` ( ( deg1 ` R ) ` F ) ) =/= ( 0g ` R ) ) ) )
21 20 3ad2ant1 
 |-  ( ( R e. DivRing /\ F e. B /\ F =/= .0. ) -> ( ( ( coe1 ` F ) ` ( ( deg1 ` R ) ` F ) ) e. ( Unit ` R ) <-> ( ( ( coe1 ` F ) ` ( ( deg1 ` R ) ` F ) ) e. ( Base ` R ) /\ ( ( coe1 ` F ) ` ( ( deg1 ` R ) ` F ) ) =/= ( 0g ` R ) ) ) )
22 15 18 21 mpbir2and 
 |-  ( ( R e. DivRing /\ F e. B /\ F =/= .0. ) -> ( ( coe1 ` F ) ` ( ( deg1 ` R ) ` F ) ) e. ( Unit ` R ) )
23 1 2 3 12 4 19 isuc1p 
 |-  ( F e. C <-> ( F e. B /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( ( deg1 ` R ) ` F ) ) e. ( Unit ` R ) ) )
24 5 6 22 23 syl3anbrc 
 |-  ( ( R e. DivRing /\ F e. B /\ F =/= .0. ) -> F e. C )