Theorem deg1sclle

Description: A scalar polynomial has nonpositive degree. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypotheses	deg1sclle.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1sclle.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1sclle.k	$$⊢K={\mathrm{Base}}_R$$
	deg1sclle.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
Assertion	deg1sclle	$$⊢\left(R\in \mathrm{Ring}\wedge F\in K\right)\to D\left(A\left(F\right)\right)\le 0$$

Proof

Step	Hyp	Ref	Expression
1		deg1sclle.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1sclle.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		deg1sclle.k	$$⊢K={\mathrm{Base}}_R$$
4		deg1sclle.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
5	2 4 3	ply1sclid	$$⊢\left(R\in \mathrm{Ring}\wedge F\in K\right)\to F={\mathrm{coe}}_1\left(A\left(F\right)\right)\left(0\right)$$
6	5	fveq2d	$$⊢\left(R\in \mathrm{Ring}\wedge F\in K\right)\to A\left(F\right)=A\left({\mathrm{coe}}_1\left(A\left(F\right)\right)\left(0\right)\right)$$
7		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
8	2 4 3 7	ply1sclcl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in K\right)\to A\left(F\right)\in {\mathrm{Base}}_P$$
9	1 2 7 4	deg1le0	$$⊢\left(R\in \mathrm{Ring}\wedge A\left(F\right)\in {\mathrm{Base}}_P\right)\to \left(D\left(A\left(F\right)\right)\le 0\leftrightarrow A\left(F\right)=A\left({\mathrm{coe}}_1\left(A\left(F\right)\right)\left(0\right)\right)\right)$$
10	8 9	syldan	$$⊢\left(R\in \mathrm{Ring}\wedge F\in K\right)\to \left(D\left(A\left(F\right)\right)\le 0\leftrightarrow A\left(F\right)=A\left({\mathrm{coe}}_1\left(A\left(F\right)\right)\left(0\right)\right)\right)$$
11	6 10	mpbird	$$⊢\left(R\in \mathrm{Ring}\wedge F\in K\right)\to D\left(A\left(F\right)\right)\le 0$$