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

Metamath Proof Explorer

Definition df-deg1

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 𝑟 ) )