Theorem deg1scl

Description: A nonzero scalar polynomial has zero 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 )
	deg1scl.z	|- .0. = ( 0g ` R )
Assertion	deg1scl	|- ( ( R e. Ring /\ F e. K /\ F =/= .0. ) -> ( 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		deg1scl.z	|- .0. = ( 0g ` R )
6	1 2 3 4	deg1sclle	|- ( ( R e. Ring /\ F e. K ) -> ( D ` ( A ` F ) ) <_ 0 )
7	6	3adant3	|- ( ( R e. Ring /\ F e. K /\ F =/= .0. ) -> ( D ` ( A ` F ) ) <_ 0 )
8		simp1	|- ( ( R e. Ring /\ F e. K /\ F =/= .0. ) -> R e. Ring )
9		eqid	|- ( Base ` P ) = ( Base ` P )
10	2 4 3 9	ply1sclcl	|- ( ( R e. Ring /\ F e. K ) -> ( A ` F ) e. ( Base ` P ) )
11	10	3adant3	|- ( ( R e. Ring /\ F e. K /\ F =/= .0. ) -> ( A ` F ) e. ( Base ` P ) )
12		eqid	|- ( 0g ` P ) = ( 0g ` P )
13	2 4 5 12 3	ply1scln0	|- ( ( R e. Ring /\ F e. K /\ F =/= .0. ) -> ( A ` F ) =/= ( 0g ` P ) )
14	1 2 12 9	deg1nn0cl	|- ( ( R e. Ring /\ ( A ` F ) e. ( Base ` P ) /\ ( A ` F ) =/= ( 0g ` P ) ) -> ( D ` ( A ` F ) ) e. NN0 )
15	8 11 13 14	syl3anc	|- ( ( R e. Ring /\ F e. K /\ F =/= .0. ) -> ( D ` ( A ` F ) ) e. NN0 )
16		nn0le0eq0	|- ( ( D ` ( A ` F ) ) e. NN0 -> ( ( D ` ( A ` F ) ) <_ 0 <-> ( D ` ( A ` F ) ) = 0 ) )
17	15 16	syl	|- ( ( R e. Ring /\ F e. K /\ F =/= .0. ) -> ( ( D ` ( A ` F ) ) <_ 0 <-> ( D ` ( A ` F ) ) = 0 ) )
18	7 17	mpbid	|- ( ( R e. Ring /\ F e. K /\ F =/= .0. ) -> ( D ` ( A ` F ) ) = 0 )