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 ) ) ) )