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

Metamath Proof Explorer

Theorem deg1le0

Description: A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 deg1le0.d 
 |-  D = ( deg1 ` R )
2 deg1le0.p 
 |-  P = ( Poly1 ` R )
3 deg1le0.b 
 |-  B = ( Base ` P )
4 deg1le0.a 
 |-  A = ( algSc ` P )
5 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
6 1 deg1fval 
 |-  D = ( 1o mDeg R )
7 1on 
 |-  1o e. On
8 7 a1i 
 |-  ( ( R e. Ring /\ F e. B ) -> 1o e. On )
9 simpl 
 |-  ( ( R e. Ring /\ F e. B ) -> R e. Ring )
10 2 3 ply1bas 
 |-  B = ( Base ` ( 1o mPoly R ) )
11 2 4 ply1ascl 
 |-  A = ( algSc ` ( 1o mPoly R ) )
12 simpr 
 |-  ( ( R e. Ring /\ F e. B ) -> F e. B )
13 5 6 8 9 10 11 12 mdegle0 
 |-  ( ( R e. Ring /\ F e. B ) -> ( ( D ` F ) <_ 0 <-> F = ( A ` ( F ` ( 1o X. { 0 } ) ) ) ) )
14 0nn0 
 |-  0 e. NN0
15 eqid 
 |-  ( coe1 ` F ) = ( coe1 ` F )
16 15 coe1fv 
 |-  ( ( F e. B /\ 0 e. NN0 ) -> ( ( coe1 ` F ) ` 0 ) = ( F ` ( 1o X. { 0 } ) ) )
17 12 14 16 sylancl 
 |-  ( ( R e. Ring /\ F e. B ) -> ( ( coe1 ` F ) ` 0 ) = ( F ` ( 1o X. { 0 } ) ) )
18 17 fveq2d 
 |-  ( ( R e. Ring /\ F e. B ) -> ( A ` ( ( coe1 ` F ) ` 0 ) ) = ( A ` ( F ` ( 1o X. { 0 } ) ) ) )
19 18 eqeq2d 
 |-  ( ( R e. Ring /\ F e. B ) -> ( F = ( A ` ( ( coe1 ` F ) ` 0 ) ) <-> F = ( A ` ( F ` ( 1o X. { 0 } ) ) ) ) )
20 13 19 bitr4d 
 |-  ( ( R e. Ring /\ F e. B ) -> ( ( D ` F ) <_ 0 <-> F = ( A ` ( ( coe1 ` F ) ` 0 ) ) ) )