Metamath Proof Explorer


Theorem mon1pldg

Description: Unitic polynomials have one leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses mon1pldg.d
|- D = ( deg1 ` R )
mon1pldg.o
|- .1. = ( 1r ` R )
mon1pldg.m
|- M = ( Monic1p ` R )
Assertion mon1pldg
|- ( F e. M -> ( ( coe1 ` F ) ` ( D ` F ) ) = .1. )

Proof

Step Hyp Ref Expression
1 mon1pldg.d
 |-  D = ( deg1 ` R )
2 mon1pldg.o
 |-  .1. = ( 1r ` R )
3 mon1pldg.m
 |-  M = ( Monic1p ` R )
4 eqid
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
5 eqid
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
6 eqid
 |-  ( 0g ` ( Poly1 ` R ) ) = ( 0g ` ( Poly1 ` R ) )
7 4 5 6 1 3 2 ismon1p
 |-  ( F e. M <-> ( F e. ( Base ` ( Poly1 ` R ) ) /\ F =/= ( 0g ` ( Poly1 ` R ) ) /\ ( ( coe1 ` F ) ` ( D ` F ) ) = .1. ) )
8 7 simp3bi
 |-  ( F e. M -> ( ( coe1 ` F ) ` ( D ` F ) ) = .1. )