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		eqid	|- ( PwSer1 ` R ) = ( PwSer1 ` R )
11	2 10 3	ply1bas	|- B = ( Base ` ( 1o mPoly R ) )
12	2 4	ply1ascl	|- A = ( algSc ` ( 1o mPoly R ) )
13		simpr	|- ( ( R e. Ring /\ F e. B ) -> F e. B )
14	5 6 8 9 11 12 13	mdegle0	|- ( ( R e. Ring /\ F e. B ) -> ( ( D ` F ) <_ 0 <-> F = ( A ` ( F ` ( 1o X. { 0 } ) ) ) ) )
15		0nn0	|- 0 e. NN0
16		eqid	|- ( coe1 ` F ) = ( coe1 ` F )
17	16	coe1fv	|- ( ( F e. B /\ 0 e. NN0 ) -> ( ( coe1 ` F ) ` 0 ) = ( F ` ( 1o X. { 0 } ) ) )
18	13 15 17	sylancl	|- ( ( R e. Ring /\ F e. B ) -> ( ( coe1 ` F ) ` 0 ) = ( F ` ( 1o X. { 0 } ) ) )
19	18	fveq2d	|- ( ( R e. Ring /\ F e. B ) -> ( A ` ( ( coe1 ` F ) ` 0 ) ) = ( A ` ( F ` ( 1o X. { 0 } ) ) ) )
20	19	eqeq2d	|- ( ( R e. Ring /\ F e. B ) -> ( F = ( A ` ( ( coe1 ` F ) ` 0 ) ) <-> F = ( A ` ( F ` ( 1o X. { 0 } ) ) ) ) )
21	14 20	bitr4d	|- ( ( R e. Ring /\ F e. B ) -> ( ( D ` F ) <_ 0 <-> F = ( A ` ( ( coe1 ` F ) ` 0 ) ) ) )