Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mnc Structured version   Visualization version   GIF version

Definition df-mnc 38223
Description: Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.)
Assertion
Ref Expression
df-mnc Monic = (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1})
Distinct variable group:   𝑠,𝑝

Detailed syntax breakdown of Definition df-mnc
StepHypRef Expression
1 cmnc 38221 . 2 class Monic
2 vs . . 3 setvar 𝑠
3 cc 10146 . . . 4 class
43cpw 4302 . . 3 class 𝒫 ℂ
5 vp . . . . . . . 8 setvar 𝑝
65cv 1631 . . . . . . 7 class 𝑝
7 cdgr 24162 . . . . . . 7 class deg
86, 7cfv 6049 . . . . . 6 class (deg‘𝑝)
9 ccoe 24161 . . . . . . 7 class coeff
106, 9cfv 6049 . . . . . 6 class (coeff‘𝑝)
118, 10cfv 6049 . . . . 5 class ((coeff‘𝑝)‘(deg‘𝑝))
12 c1 10149 . . . . 5 class 1
1311, 12wceq 1632 . . . 4 wff ((coeff‘𝑝)‘(deg‘𝑝)) = 1
142cv 1631 . . . . 5 class 𝑠
15 cply 24159 . . . . 5 class Poly
1614, 15cfv 6049 . . . 4 class (Poly‘𝑠)
1713, 5, 16crab 3054 . . 3 class {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1}
182, 4, 17cmpt 4881 . 2 class (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1})
191, 18wceq 1632 1 wff Monic = (𝑠 ∈ 𝒫 ℂ ↦ {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1})
Colors of variables: wff setvar class
This definition is referenced by:  elmnc  38226
  Copyright terms: Public domain W3C validator