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

Metamath Proof Explorer

Theorem deg1scl

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

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

Proof

Step Hyp Ref Expression
1 deg1sclle.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2 deg1sclle.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 deg1sclle.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 deg1sclle.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
5 deg1scl.z ⊢ 0 = ( 0g ‘ 𝑅 )
6 1 2 3 4 deg1sclle ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ≤ 0 )
7 6 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ≤ 0 )
8 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → 𝑅 ∈ Ring )
9 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
10 2 4 3 9 ply1sclcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ) → ( 𝐴 ‘ 𝐹 ) ∈ ( Base ‘ 𝑃 ) )
11 10 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → ( 𝐴 ‘ 𝐹 ) ∈ ( Base ‘ 𝑃 ) )
12 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
13 2 4 5 12 3 ply1scln0 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → ( 𝐴 ‘ 𝐹 ) ≠ ( 0g ‘ 𝑃 ) )
14 1 2 12 9 deg1nn0cl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ‘ 𝐹 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐴 ‘ 𝐹 ) ≠ ( 0g ‘ 𝑃 ) ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ∈ ℕ0 )
15 8 11 13 14 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ∈ ℕ0 )
16 nn0le0eq0 ⊢ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ∈ ℕ0 → ( ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ≤ 0 ↔ ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) = 0 ) )
17 15 16 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → ( ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ≤ 0 ↔ ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) = 0 ) )
18 7 17 mpbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) = 0 )