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