Metamath Proof Explorer
Description: Define the degree of a univariate polynomial. (Contributed by Stefan
O'Rear, 23-Mar-2015)
|
|
Ref |
Expression |
|
Assertion |
df-deg1 |
⊢ deg1 = ( 𝑟 ∈ V ↦ ( 1o mDeg 𝑟 ) ) |
Detailed syntax breakdown
Step |
Hyp |
Ref |
Expression |
0 |
|
cdg1 |
⊢ deg1 |
1 |
|
vr |
⊢ 𝑟 |
2 |
|
cvv |
⊢ V |
3 |
|
c1o |
⊢ 1o |
4 |
|
cmdg |
⊢ mDeg |
5 |
1
|
cv |
⊢ 𝑟 |
6 |
3 5 4
|
co |
⊢ ( 1o mDeg 𝑟 ) |
7 |
1 2 6
|
cmpt |
⊢ ( 𝑟 ∈ V ↦ ( 1o mDeg 𝑟 ) ) |
8 |
0 7
|
wceq |
⊢ deg1 = ( 𝑟 ∈ V ↦ ( 1o mDeg 𝑟 ) ) |