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

Metamath Proof Explorer

Theorem deg1sclle

Description: A scalar polynomial has nonpositive degree. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses deg1sclle.d 
|- D = ( deg1 ` R )
deg1sclle.p 
|- P = ( Poly1 ` R )
deg1sclle.k 
|- K = ( Base ` R )
deg1sclle.a 
|- A = ( algSc ` P )
Assertion deg1sclle 
|- ( ( R e. Ring /\ F e. K ) -> ( D ` ( A ` F ) ) <_ 0 )

Proof

Step Hyp Ref Expression
1 deg1sclle.d 
 |-  D = ( deg1 ` R )
2 deg1sclle.p 
 |-  P = ( Poly1 ` R )
3 deg1sclle.k 
 |-  K = ( Base ` R )
4 deg1sclle.a 
 |-  A = ( algSc ` P )
5 2 4 3 ply1sclid 
 |-  ( ( R e. Ring /\ F e. K ) -> F = ( ( coe1 ` ( A ` F ) ) ` 0 ) )
6 5 fveq2d 
 |-  ( ( R e. Ring /\ F e. K ) -> ( A ` F ) = ( A ` ( ( coe1 ` ( A ` F ) ) ` 0 ) ) )
7 eqid 
 |-  ( Base ` P ) = ( Base ` P )
8 2 4 3 7 ply1sclcl 
 |-  ( ( R e. Ring /\ F e. K ) -> ( A ` F ) e. ( Base ` P ) )
9 1 2 7 4 deg1le0 
 |-  ( ( R e. Ring /\ ( A ` F ) e. ( Base ` P ) ) -> ( ( D ` ( A ` F ) ) <_ 0 <-> ( A ` F ) = ( A ` ( ( coe1 ` ( A ` F ) ) ` 0 ) ) ) )
10 8 9 syldan 
 |-  ( ( R e. Ring /\ F e. K ) -> ( ( D ` ( A ` F ) ) <_ 0 <-> ( A ` F ) = ( A ` ( ( coe1 ` ( A ` F ) ) ` 0 ) ) ) )
11 6 10 mpbird 
 |-  ( ( R e. Ring /\ F e. K ) -> ( D ` ( A ` F ) ) <_ 0 )