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

Metamath Proof Explorer

Theorem mdegxrf

Description: Functionality of polynomial degree in the extended reals. (Contributed by Stefan O'Rear, 19-Mar-2015) (Proof shortened by AV, 27-Jul-2019)

Ref Expression
Hypotheses mdegxrcl.d ⊢ D = I mDeg R
mdegxrcl.p ⊢ P = I mPoly R
mdegxrcl.b ⊢ B = Base P
Assertion mdegxrf ⊢ D : B ⟶ ℝ *

Proof

Step Hyp Ref Expression
1 mdegxrcl.d ⊢ D = I mDeg R
2 mdegxrcl.p ⊢ P = I mPoly R
3 mdegxrcl.b ⊢ B = Base P
4 xrltso ⊢ < Or ℝ *
5 4 supex ⊢ sup y ∈ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ⟼ ∑ ℂ fld y z supp 0 R ℝ * < ∈ V
6 eqid ⊢ 0 R = 0 R
7 eqid ⊢ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin = x ∈ ℕ 0 I | x -1 ℕ ∈ Fin
8 eqid ⊢ y ∈ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ⟼ ∑ ℂ fld y = y ∈ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ⟼ ∑ ℂ fld y
9 1 2 3 6 7 8 mdegfval ⊢ D = z ∈ B ⟼ sup y ∈ x ∈ ℕ 0 I | x -1 ℕ ∈ Fin ⟼ ∑ ℂ fld y z supp 0 R ℝ * <
10 5 9 fnmpti ⊢ D Fn B
11 1 2 3 mdegxrcl ⊢ f ∈ B → D ⁡ f ∈ ℝ *
12 11 rgen ⊢ ∀ f ∈ B D ⁡ f ∈ ℝ *
13 ffnfv ⊢ D : B ⟶ ℝ * ↔ D Fn B ∧ ∀ f ∈ B D ⁡ f ∈ ℝ *
14 10 12 13 mpbir2an ⊢ D : B ⟶ ℝ *