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		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
11	2 10 3	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
12	2 4	ply1ascl	⊢ 𝐴 = ( algSc ‘ ( 1o mPoly 𝑅 ) )
13		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → 𝐹 ∈ 𝐵 )
14	5 6 8 9 11 12 13	mdegle0	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 0 ↔ 𝐹 = ( 𝐴 ‘ ( 𝐹 ‘ ( 1o × { 0 } ) ) ) ) )
15		0nn0	⊢ 0 ∈ ℕ0
16		eqid	⊢ ( coe1 ‘ 𝐹 ) = ( coe1 ‘ 𝐹 )
17	16	coe1fv	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = ( 𝐹 ‘ ( 1o × { 0 } ) ) )
18	13 15 17	sylancl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = ( 𝐹 ‘ ( 1o × { 0 } ) ) )
19	18	fveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( 𝐴 ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) = ( 𝐴 ‘ ( 𝐹 ‘ ( 1o × { 0 } ) ) ) )
20	19	eqeq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( 𝐹 = ( 𝐴 ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) ↔ 𝐹 = ( 𝐴 ‘ ( 𝐹 ‘ ( 1o × { 0 } ) ) ) ) )
21	14 20	bitr4d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 0 ↔ 𝐹 = ( 𝐴 ‘ ( ( coe1 ‘ 𝐹 ) ‘ 0 ) ) ) )