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 41865
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 41863 . 2 class Monic
2 vs . . 3 setvar 𝑠
3 cc 11107 . . . 4 class β„‚
43cpw 4602 . . 3 class 𝒫 β„‚
5 vp . . . . . . . 8 setvar 𝑝
65cv 1540 . . . . . . 7 class 𝑝
7 cdgr 25700 . . . . . . 7 class deg
86, 7cfv 6543 . . . . . 6 class (degβ€˜π‘)
9 ccoe 25699 . . . . . . 7 class coeff
106, 9cfv 6543 . . . . . 6 class (coeffβ€˜π‘)
118, 10cfv 6543 . . . . 5 class ((coeffβ€˜π‘)β€˜(degβ€˜π‘))
12 c1 11110 . . . . 5 class 1
1311, 12wceq 1541 . . . 4 wff ((coeffβ€˜π‘)β€˜(degβ€˜π‘)) = 1
142cv 1540 . . . . 5 class 𝑠
15 cply 25697 . . . . 5 class Poly
1614, 15cfv 6543 . . . 4 class (Polyβ€˜π‘ )
1713, 5, 16crab 3432 . . 3 class {𝑝 ∈ (Polyβ€˜π‘ ) ∣ ((coeffβ€˜π‘)β€˜(degβ€˜π‘)) = 1}
182, 4, 17cmpt 5231 . 2 class (𝑠 ∈ 𝒫 β„‚ ↦ {𝑝 ∈ (Polyβ€˜π‘ ) ∣ ((coeffβ€˜π‘)β€˜(degβ€˜π‘)) = 1})
191, 18wceq 1541 1 wff Monic = (𝑠 ∈ 𝒫 β„‚ ↦ {𝑝 ∈ (Polyβ€˜π‘ ) ∣ ((coeffβ€˜π‘)β€˜(degβ€˜π‘)) = 1})
Colors of variables: wff setvar class
This definition is referenced by:  elmnc  41868
  Copyright terms: Public domain W3C validator