Definition df-mnc

Description: Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014)

	Ref	Expression
Assertion	df-mnc	⊢ Monic = ( 𝑠 ∈ 𝒫 ℂ ↦ { 𝑝 ∈ ( Poly ‘ 𝑠 ) ∣ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmnc	⊢ Monic
1		vs	⊢ 𝑠
2		cc	⊢ ℂ
3	2	cpw	⊢ 𝒫 ℂ
4		vp	⊢ 𝑝
5		cply	⊢ Poly
6	1	cv	⊢ 𝑠
7	6 5	cfv	⊢ ( Poly ‘ 𝑠 )
8		ccoe	⊢ coeff
9	4	cv	⊢ 𝑝
10	9 8	cfv	⊢ ( coeff ‘ 𝑝 )
11		cdgr	⊢ deg
12	9 11	cfv	⊢ ( deg ‘ 𝑝 )
13	12 10	cfv	⊢ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) )
14		c1	⊢ 1
15	13 14	wceq	⊢ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1
16	15 4 7	crab	⊢ { 𝑝 ∈ ( Poly ‘ 𝑠 ) ∣ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 }
17	1 3 16	cmpt	⊢ ( 𝑠 ∈ 𝒫 ℂ ↦ { 𝑝 ∈ ( Poly ‘ 𝑠 ) ∣ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 } )
18	0 17	wceq	⊢ Monic = ( 𝑠 ∈ 𝒫 ℂ ↦ { 𝑝 ∈ ( Poly ‘ 𝑠 ) ∣ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 } )