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

Metamath Proof Explorer

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 )