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

Metamath Proof Explorer

Theorem 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 ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
deg1le0.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
deg1le0.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
deg1le0.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
Assertion deg1le0 ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 0 ↔ 𝐹 = ( 𝐴 ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 deg1le0.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2 deg1le0.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 deg1le0.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 deg1le0.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
5 eqid ⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
6 1 deg1fval ⊢ 𝐷 = ( 1o mDeg 𝑅 )
7 1on ⊢ 1o ∈ On
8 7 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → 1o ∈ On )
9 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → 𝑅 ∈ Ring )
10 2 3 ply1bas ⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
11 2 4 ply1ascl ⊢ 𝐴 = ( algSc ‘ ( 1o mPoly 𝑅 ) )
12 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → 𝐹 ∈ 𝐵 )
13 5 6 8 9 10 11 12 mdegle0 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 0 ↔ 𝐹 = ( 𝐴 ‘ ( 𝐹 ‘ ( 1o × { 0 } ) ) ) ) )
14 0nn0 ⊢ 0 ∈ ℕ0
15 eqid ⊢ ( coe1 ‘ 𝐹 ) = ( coe1 ‘ 𝐹 )
16 15 coe1fv ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = ( 𝐹 ‘ ( 1o × { 0 } ) ) )
17 12 14 16 sylancl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = ( 𝐹 ‘ ( 1o × { 0 } ) ) )
18 17 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( 𝐴 ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) = ( 𝐴 ‘ ( 𝐹 ‘ ( 1o × { 0 } ) ) ) )
19 18 eqeq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( 𝐹 = ( 𝐴 ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) ↔ 𝐹 = ( 𝐴 ‘ ( 𝐹 ‘ ( 1o × { 0 } ) ) ) ) )
20 13 19 bitr4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 0 ↔ 𝐹 = ( 𝐴 ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) ) )