deg1scl

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

	Ref	Expression
Hypotheses	deg1sclle.d	$⊢ D = \deg_{1} (R)$
	deg1sclle.p	$⊢ P = {Poly}_{1} (R)$
	deg1sclle.k	$⊢ K = {Base}_{R}$
	deg1sclle.a	$⊢ A = algSc (P)$
	deg1scl.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	deg1scl	$⊢ (R \in Ring \land F \in K \land F \neq \underset{˙}{0}) \to D (A (F)) = 0$

Step	Hyp	Ref	Expression
1		deg1sclle.d	$⊢ D = \deg_{1} (R)$
2		deg1sclle.p	$⊢ P = {Poly}_{1} (R)$
3		deg1sclle.k	$⊢ K = {Base}_{R}$
4		deg1sclle.a	$⊢ A = algSc (P)$
5		deg1scl.z	$⊢ \underset{˙}{0} = 0_{R}$
6	1 2 3 4	deg1sclle	$⊢ (R \in Ring \land F \in K) \to D (A (F)) \leq 0$
7	6	3adant3	$⊢ (R \in Ring \land F \in K \land F \neq \underset{˙}{0}) \to D (A (F)) \leq 0$
8		simp1	$⊢ (R \in Ring \land F \in K \land F \neq \underset{˙}{0}) \to R \in Ring$
9		eqid	$⊢ {Base}_{P} = {Base}_{P}$
10	2 4 3 9	ply1sclcl	$⊢ (R \in Ring \land F \in K) \to A (F) \in {Base}_{P}$
11	10	3adant3	$⊢ (R \in Ring \land F \in K \land F \neq \underset{˙}{0}) \to A (F) \in {Base}_{P}$
12		eqid	$⊢ 0_{P} = 0_{P}$
13	2 4 5 12 3	ply1scln0	$⊢ (R \in Ring \land F \in K \land F \neq \underset{˙}{0}) \to A (F) \neq 0_{P}$
14	1 2 12 9	deg1nn0cl	$⊢ (R \in Ring \land A (F) \in {Base}_{P} \land A (F) \neq 0_{P}) \to D (A (F)) \in ℕ_{0}$
15	8 11 13 14	syl3anc	$⊢ (R \in Ring \land F \in K \land F \neq \underset{˙}{0}) \to D (A (F)) \in ℕ_{0}$
16		nn0le0eq0	$⊢ D (A (F)) \in ℕ_{0} \to (D (A (F)) \leq 0 \leftrightarrow D (A (F)) = 0)$
17	15 16	syl	$⊢ (R \in Ring \land F \in K \land F \neq \underset{˙}{0}) \to (D (A (F)) \leq 0 \leftrightarrow D (A (F)) = 0)$
18	7 17	mpbid	$⊢ (R \in Ring \land F \in K \land F \neq \underset{˙}{0}) \to D (A (F)) = 0$

Metamath Proof Explorer