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	2 3	ply1bas	$⊢ B = {Base}_{(1_{𝑜} mPoly R)}$
11	2 4	ply1ascl	$⊢ A = algSc (1_{𝑜} mPoly R)$
12		simpr	$⊢ (R \in Ring \land F \in B) \to F \in B$
13	5 6 8 9 10 11 12	mdegle0	$⊢ (R \in Ring \land F \in B) \to (D (F) \leq 0 \leftrightarrow F = A (F (1_{𝑜} \times \{0\})))$
14		0nn0	$⊢ 0 \in ℕ_{0}$
15		eqid	$⊢ {coe}_{1} (F) = {coe}_{1} (F)$
16	15	coe1fv	$⊢ (F \in B \land 0 \in ℕ_{0}) \to {coe}_{1} (F) (0) = F (1_{𝑜} \times \{0\})$
17	12 14 16	sylancl	$⊢ (R \in Ring \land F \in B) \to {coe}_{1} (F) (0) = F (1_{𝑜} \times \{0\})$
18	17	fveq2d	$⊢ (R \in Ring \land F \in B) \to A ({coe}_{1} (F) (0)) = A (F (1_{𝑜} \times \{0\}))$
19	18	eqeq2d	$⊢ (R \in Ring \land F \in B) \to (F = A ({coe}_{1} (F) (0)) \leftrightarrow F = A (F (1_{𝑜} \times \{0\})))$
20	13 19	bitr4d	$⊢ (R \in Ring \land F \in B) \to (D (F) \leq 0 \leftrightarrow F = A ({coe}_{1} (F) (0)))$

Metamath Proof Explorer