Theorem deg1le0eq0

Description: A polynomial with nonpositive degree is the zero polynomial iff its constant term is zero. Biconditional version of deg1scl . (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	deg1sclb.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1sclb.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1sclb.z	⊢ 0 = ( 0g ‘ 𝑅 )
	deg1sclb.1	⊢ 𝐵 = ( Base ‘ 𝑃 )
	deg1sclb.2	⊢ 𝑂 = ( 0g ‘ 𝑃 )
	deg1sclb.3	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	deg1sclb.4	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	deg1sclb.5	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 0 )
Assertion	deg1le0eq0	⊢ ( 𝜑 → ( 𝐹 = 𝑂 ↔ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		deg1sclb.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1sclb.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1sclb.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		deg1sclb.1	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		deg1sclb.2	⊢ 𝑂 = ( 0g ‘ 𝑃 )
6		deg1sclb.3	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		deg1sclb.4	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
8		deg1sclb.5	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 0 )
9		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
10	1 2 4 9	deg1le0	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 0 ↔ 𝐹 = ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) ) )
11	10	biimpa	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐷 ‘ 𝐹 ) ≤ 0 ) → 𝐹 = ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) )
12	6 7 8 11	syl21anc	⊢ ( 𝜑 → 𝐹 = ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝐹 = 𝑂 ) → 𝐹 = ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) )
14		simpr	⊢ ( ( 𝜑 ∧ 𝐹 = 𝑂 ) → 𝐹 = 𝑂 )
15	13 14	eqtr3d	⊢ ( ( 𝜑 ∧ 𝐹 = 𝑂 ) → ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) = 𝑂 )
16	6	adantr	⊢ ( ( 𝜑 ∧ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ≠ 0 ) → 𝑅 ∈ Ring )
17		0nn0	⊢ 0 ∈ ℕ0
18		eqid	⊢ ( coe1 ‘ 𝐹 ) = ( coe1 ‘ 𝐹 )
19		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
20	18 4 2 19	coe1fvalcl	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
21	7 17 20	sylancl	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ≠ 0 ) → ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
23		simpr	⊢ ( ( 𝜑 ∧ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ≠ 0 ) → ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ≠ 0 )
24	2 9 3 5 19	ply1scln0	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ≠ 0 ) → ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) ≠ 𝑂 )
25	16 22 23 24	syl3anc	⊢ ( ( 𝜑 ∧ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ≠ 0 ) → ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) ≠ 𝑂 )
26	25	ex	⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ≠ 0 → ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) ≠ 𝑂 ) )
27	26	necon4d	⊢ ( 𝜑 → ( ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) = 𝑂 → ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = 0 ) )
28	27	imp	⊢ ( ( 𝜑 ∧ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) = 𝑂 ) → ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = 0 )
29	15 28	syldan	⊢ ( ( 𝜑 ∧ 𝐹 = 𝑂 ) → ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = 0 )
30	12	adantr	⊢ ( ( 𝜑 ∧ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = 0 ) → 𝐹 = ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) )
31		simpr	⊢ ( ( 𝜑 ∧ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = 0 ) → ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = 0 )
32	31	fveq2d	⊢ ( ( 𝜑 ∧ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = 0 ) → ( ( algSc ‘ 𝑃 ) ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) = ( ( algSc ‘ 𝑃 ) ‘ 0 ) )
33	2 9 3 5 6	ply1ascl0	⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ 0 ) = 𝑂 )
34	33	adantr	⊢ ( ( 𝜑 ∧ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = 0 ) → ( ( algSc ‘ 𝑃 ) ‘ 0 ) = 𝑂 )
35	30 32 34	3eqtrd	⊢ ( ( 𝜑 ∧ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = 0 ) → 𝐹 = 𝑂 )
36	29 35	impbida	⊢ ( 𝜑 → ( 𝐹 = 𝑂 ↔ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = 0 ) )