MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mon1 Structured version   Visualization version   GIF version

Definition df-mon1 24651
Description: Define the set of monic univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
Assertion
Ref Expression
df-mon1 Monic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1𝑟)) ∧ ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) = (1r𝑟))})
Distinct variable group:   𝑓,𝑟

Detailed syntax breakdown of Definition df-mon1
StepHypRef Expression
1 cmn1 24646 . 2 class Monic1p
2 vr . . 3 setvar 𝑟
3 cvv 3492 . . 3 class V
4 vf . . . . . . 7 setvar 𝑓
54cv 1527 . . . . . 6 class 𝑓
62cv 1527 . . . . . . . 8 class 𝑟
7 cpl1 20273 . . . . . . . 8 class Poly1
86, 7cfv 6348 . . . . . . 7 class (Poly1𝑟)
9 c0g 16701 . . . . . . 7 class 0g
108, 9cfv 6348 . . . . . 6 class (0g‘(Poly1𝑟))
115, 10wne 3013 . . . . 5 wff 𝑓 ≠ (0g‘(Poly1𝑟))
12 cdg1 24575 . . . . . . . . 9 class deg1
136, 12cfv 6348 . . . . . . . 8 class ( deg1𝑟)
145, 13cfv 6348 . . . . . . 7 class (( deg1𝑟)‘𝑓)
15 cco1 20274 . . . . . . . 8 class coe1
165, 15cfv 6348 . . . . . . 7 class (coe1𝑓)
1714, 16cfv 6348 . . . . . 6 class ((coe1𝑓)‘(( deg1𝑟)‘𝑓))
18 cur 19180 . . . . . . 7 class 1r
196, 18cfv 6348 . . . . . 6 class (1r𝑟)
2017, 19wceq 1528 . . . . 5 wff ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) = (1r𝑟)
2111, 20wa 396 . . . 4 wff (𝑓 ≠ (0g‘(Poly1𝑟)) ∧ ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) = (1r𝑟))
22 cbs 16471 . . . . 5 class Base
238, 22cfv 6348 . . . 4 class (Base‘(Poly1𝑟))
2421, 4, 23crab 3139 . . 3 class {𝑓 ∈ (Base‘(Poly1𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1𝑟)) ∧ ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) = (1r𝑟))}
252, 3, 24cmpt 5137 . 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1𝑟)) ∧ ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) = (1r𝑟))})
261, 25wceq 1528 1 wff Monic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1𝑟)) ∧ ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) = (1r𝑟))})
Colors of variables: wff setvar class
This definition is referenced by:  mon1pval  24662
  Copyright terms: Public domain W3C validator