MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-deg1 Structured version   Visualization version   GIF version

Definition df-deg1 23797
Description: Define the degree of a univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.)
Assertion
Ref Expression
df-deg1 deg1 = (𝑟 ∈ V ↦ (1𝑜 mDeg 𝑟))

Detailed syntax breakdown of Definition df-deg1
StepHypRef Expression
1 cdg1 23795 . 2 class deg1
2 vr . . 3 setvar 𝑟
3 cvv 3195 . . 3 class V
4 c1o 7538 . . . 4 class 1𝑜
52cv 1480 . . . 4 class 𝑟
6 cmdg 23794 . . . 4 class mDeg
74, 5, 6co 6635 . . 3 class (1𝑜 mDeg 𝑟)
82, 3, 7cmpt 4720 . 2 class (𝑟 ∈ V ↦ (1𝑜 mDeg 𝑟))
91, 8wceq 1481 1 wff deg1 = (𝑟 ∈ V ↦ (1𝑜 mDeg 𝑟))
Colors of variables: wff setvar class
This definition is referenced by:  deg1fval  23821
  Copyright terms: Public domain W3C validator