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