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

Definition df-uc1p 23872
 Description: Define the set of unitic univariate polynomials, as the polynomials with an invertible leading coefficient. This is not a standard concept but is useful to us as the set of polynomials which can be used as the divisor in the polynomial division theorem ply1divalg 23878. (Contributed by Stefan O'Rear, 28-Mar-2015.)
Assertion
Ref Expression
df-uc1p Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1𝑟)) ∧ ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
Distinct variable group:   𝑓,𝑟

Detailed syntax breakdown of Definition df-uc1p
StepHypRef Expression
1 cuc1p 23867 . 2 class Unic1p
2 vr . . 3 setvar 𝑟
3 cvv 3195 . . 3 class V
4 vf . . . . . . 7 setvar 𝑓
54cv 1480 . . . . . 6 class 𝑓
62cv 1480 . . . . . . . 8 class 𝑟
7 cpl1 19528 . . . . . . . 8 class Poly1
86, 7cfv 5876 . . . . . . 7 class (Poly1𝑟)
9 c0g 16081 . . . . . . 7 class 0g
108, 9cfv 5876 . . . . . 6 class (0g‘(Poly1𝑟))
115, 10wne 2791 . . . . 5 wff 𝑓 ≠ (0g‘(Poly1𝑟))
12 cdg1 23795 . . . . . . . . 9 class deg1
136, 12cfv 5876 . . . . . . . 8 class ( deg1𝑟)
145, 13cfv 5876 . . . . . . 7 class (( deg1𝑟)‘𝑓)
15 cco1 19529 . . . . . . . 8 class coe1
165, 15cfv 5876 . . . . . . 7 class (coe1𝑓)
1714, 16cfv 5876 . . . . . 6 class ((coe1𝑓)‘(( deg1𝑟)‘𝑓))
18 cui 18620 . . . . . . 7 class Unit
196, 18cfv 5876 . . . . . 6 class (Unit‘𝑟)
2017, 19wcel 1988 . . . . 5 wff ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) ∈ (Unit‘𝑟)
2111, 20wa 384 . . . 4 wff (𝑓 ≠ (0g‘(Poly1𝑟)) ∧ ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22 cbs 15838 . . . . 5 class Base
238, 22cfv 5876 . . . 4 class (Base‘(Poly1𝑟))
2421, 4, 23crab 2913 . . 3 class {𝑓 ∈ (Base‘(Poly1𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1𝑟)) ∧ ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
252, 3, 24cmpt 4720 . 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1𝑟)) ∧ ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
261, 25wceq 1481 1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1𝑟)) ∧ ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
 Colors of variables: wff setvar class This definition is referenced by:  uc1pval  23880
 Copyright terms: Public domain W3C validator