Theorem deg1sclle

Description: A scalar polynomial has nonpositive degree. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypotheses	deg1sclle.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1sclle.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1sclle.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	deg1sclle.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
Assertion	deg1sclle	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ≤ 0 )

Proof

Step	Hyp	Ref	Expression
1		deg1sclle.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1sclle.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1sclle.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		deg1sclle.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
5	2 4 3	ply1sclid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ) → 𝐹 = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) )
6	5	fveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ) → ( 𝐴 ‘ 𝐹 ) = ( 𝐴 ‘ ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) ) )
7		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
8	2 4 3 7	ply1sclcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ) → ( 𝐴 ‘ 𝐹 ) ∈ ( Base ‘ 𝑃 ) )
9	1 2 7 4	deg1le0	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ‘ 𝐹 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ≤ 0 ↔ ( 𝐴 ‘ 𝐹 ) = ( 𝐴 ‘ ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) ) ) )
10	8 9	syldan	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ) → ( ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ≤ 0 ↔ ( 𝐴 ‘ 𝐹 ) = ( 𝐴 ‘ ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) ) ) )
11	6 10	mpbird	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ≤ 0 )