Metamath Proof Explorer

Theorem mdegnn0cl

Description: Degree of a nonzero polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses mdeg0.d ⊢ D = I mDeg R
mdeg0.p ⊢ P = I mPoly R
mdeg0.z ⊢ 0 ˙ = 0 P
mdegnn0cl.b ⊢ B = Base P
Assertion mdegnn0cl ⊢ R ∈ Ring ∧ F ∈ B ∧ F ≠ 0 ˙ → D ⁡ F ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 mdeg0.d ⊢ D = I mDeg R
2 mdeg0.p ⊢ P = I mPoly R
3 mdeg0.z ⊢ 0 ˙ = 0 P
4 mdegnn0cl.b ⊢ B = Base P
5 eqid ⊢ 0 R = 0 R
6 eqid ⊢ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin = m ∈ ℕ 0 I | m -1 ℕ ∈ Fin
7 eqid ⊢ h ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin ⟼ ∑ ℂ fld h = h ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin ⟼ ∑ ℂ fld h
8 1 2 4 5 6 7 3 mdegldg ⊢ R ∈ Ring ∧ F ∈ B ∧ F ≠ 0 ˙ → ∃ x ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin F ⁡ x ≠ 0 R ∧ h ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin ⟼ ∑ ℂ fld h ⁡ x = D ⁡ F
9 6 7 tdeglem1 ⊢ h ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin ⟼ ∑ ℂ fld h : m ∈ ℕ 0 I | m -1 ℕ ∈ Fin ⟶ ℕ 0
10 9 a1i ⊢ R ∈ Ring ∧ F ∈ B ∧ F ≠ 0 ˙ → h ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin ⟼ ∑ ℂ fld h : m ∈ ℕ 0 I | m -1 ℕ ∈ Fin ⟶ ℕ 0
11 10 ffvelrnda ⊢ R ∈ Ring ∧ F ∈ B ∧ F ≠ 0 ˙ ∧ x ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin → h ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin ⟼ ∑ ℂ fld h ⁡ x ∈ ℕ 0
12 eleq1 ⊢ h ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin ⟼ ∑ ℂ fld h ⁡ x = D ⁡ F → h ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin ⟼ ∑ ℂ fld h ⁡ x ∈ ℕ 0 ↔ D ⁡ F ∈ ℕ 0
13 11 12 syl5ibcom ⊢ R ∈ Ring ∧ F ∈ B ∧ F ≠ 0 ˙ ∧ x ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin → h ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin ⟼ ∑ ℂ fld h ⁡ x = D ⁡ F → D ⁡ F ∈ ℕ 0
14 13 adantld ⊢ R ∈ Ring ∧ F ∈ B ∧ F ≠ 0 ˙ ∧ x ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin → F ⁡ x ≠ 0 R ∧ h ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin ⟼ ∑ ℂ fld h ⁡ x = D ⁡ F → D ⁡ F ∈ ℕ 0
15 14 rexlimdva ⊢ R ∈ Ring ∧ F ∈ B ∧ F ≠ 0 ˙ → ∃ x ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin F ⁡ x ≠ 0 R ∧ h ∈ m ∈ ℕ 0 I | m -1 ℕ ∈ Fin ⟼ ∑ ℂ fld h ⁡ x = D ⁡ F → D ⁡ F ∈ ℕ 0
16 8 15 mpd ⊢ R ∈ Ring ∧ F ∈ B ∧ F ≠ 0 ˙ → D ⁡ F ∈ ℕ 0