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 = \deg_{1} (R)$
	deg1le0.p	$⊢ P = {Poly}_{1} (R)$
	deg1le0.b	$⊢ B = {Base}_{P}$
	deg1le0.a	$⊢ A = algSc (P)$
Assertion	deg1le0	$⊢ (R \in Ring \land F \in B) \to (D (F) \leq 0 \leftrightarrow F = A ({coe}_{1} (F) (0)))$

Step	Hyp	Ref	Expression
1		deg1le0.d	$⊢ D = \deg_{1} (R)$
2		deg1le0.p	$⊢ P = {Poly}_{1} (R)$
3		deg1le0.b	$⊢ B = {Base}_{P}$
4		deg1le0.a	$⊢ A = algSc (P)$
5		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
6	1	deg1fval	$⊢ D = 1_{𝑜} mDeg R$
7		1on	$⊢ 1_{𝑜} \in On$
8	7	a1i	$⊢ (R \in Ring \land F \in B) \to 1_{𝑜} \in On$
9		simpl	$⊢ (R \in Ring \land F \in B) \to R \in Ring$
10		eqid	$⊢ {PwSer}_{1} (R) = {PwSer}_{1} (R)$
11	2 10 3	ply1bas	$⊢ B = {Base}_{(1_{𝑜} mPoly R)}$
12	2 4	ply1ascl	$⊢ A = algSc (1_{𝑜} mPoly R)$
13		simpr	$⊢ (R \in Ring \land F \in B) \to F \in B$
14	5 6 8 9 11 12 13	mdegle0	$⊢ (R \in Ring \land F \in B) \to (D (F) \leq 0 \leftrightarrow F = A (F (1_{𝑜} \times \{0\})))$
15		0nn0	$⊢ 0 \in ℕ_{0}$
16		eqid	$⊢ {coe}_{1} (F) = {coe}_{1} (F)$
17	16	coe1fv	$⊢ (F \in B \land 0 \in ℕ_{0}) \to {coe}_{1} (F) (0) = F (1_{𝑜} \times \{0\})$
18	13 15 17	sylancl	$⊢ (R \in Ring \land F \in B) \to {coe}_{1} (F) (0) = F (1_{𝑜} \times \{0\})$
19	18	fveq2d	$⊢ (R \in Ring \land F \in B) \to A ({coe}_{1} (F) (0)) = A (F (1_{𝑜} \times \{0\}))$
20	19	eqeq2d	$⊢ (R \in Ring \land F \in B) \to (F = A ({coe}_{1} (F) (0)) \leftrightarrow F = A (F (1_{𝑜} \times \{0\})))$
21	14 20	bitr4d	$⊢ (R \in Ring \land F \in B) \to (D (F) \leq 0 \leftrightarrow F = A ({coe}_{1} (F) (0)))$

Metamath Proof Explorer