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 41489
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 41487 . 2 class Monic
2 vs . . 3 setvar 𝑠
3 cc 11056 . . . 4 class β„‚
43cpw 4565 . . 3 class 𝒫 β„‚
5 vp . . . . . . . 8 setvar 𝑝
65cv 1541 . . . . . . 7 class 𝑝
7 cdgr 25564 . . . . . . 7 class deg
86, 7cfv 6501 . . . . . 6 class (degβ€˜π‘)
9 ccoe 25563 . . . . . . 7 class coeff
106, 9cfv 6501 . . . . . 6 class (coeffβ€˜π‘)
118, 10cfv 6501 . . . . 5 class ((coeffβ€˜π‘)β€˜(degβ€˜π‘))
12 c1 11059 . . . . 5 class 1
1311, 12wceq 1542 . . . 4 wff ((coeffβ€˜π‘)β€˜(degβ€˜π‘)) = 1
142cv 1541 . . . . 5 class 𝑠
15 cply 25561 . . . . 5 class Poly
1614, 15cfv 6501 . . . 4 class (Polyβ€˜π‘ )
1713, 5, 16crab 3410 . . 3 class {𝑝 ∈ (Polyβ€˜π‘ ) ∣ ((coeffβ€˜π‘)β€˜(degβ€˜π‘)) = 1}
182, 4, 17cmpt 5193 . 2 class (𝑠 ∈ 𝒫 β„‚ ↦ {𝑝 ∈ (Polyβ€˜π‘ ) ∣ ((coeffβ€˜π‘)β€˜(degβ€˜π‘)) = 1})
191, 18wceq 1542 1 wff Monic = (𝑠 ∈ 𝒫 β„‚ ↦ {𝑝 ∈ (Polyβ€˜π‘ ) ∣ ((coeffβ€˜π‘)β€˜(degβ€˜π‘)) = 1})
Colors of variables: wff setvar class
This definition is referenced by:  elmnc  41492
  Copyright terms: Public domain W3C validator