This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )