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 )