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

Definition df-uc1p 24127
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 24133. (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 24122 . 2 class Unic1p
2 vr . . 3 setvar 𝑟
3 cvv 3402 . . 3 class V
4 vf . . . . . . 7 setvar 𝑓
54cv 1636 . . . . . 6 class 𝑓
62cv 1636 . . . . . . . 8 class 𝑟
7 cpl1 19774 . . . . . . . 8 class Poly1
86, 7cfv 6110 . . . . . . 7 class (Poly1𝑟)
9 c0g 16324 . . . . . . 7 class 0g
108, 9cfv 6110 . . . . . 6 class (0g‘(Poly1𝑟))
115, 10wne 2989 . . . . 5 wff 𝑓 ≠ (0g‘(Poly1𝑟))
12 cdg1 24050 . . . . . . . . 9 class deg1
136, 12cfv 6110 . . . . . . . 8 class ( deg1𝑟)
145, 13cfv 6110 . . . . . . 7 class (( deg1𝑟)‘𝑓)
15 cco1 19775 . . . . . . . 8 class coe1
165, 15cfv 6110 . . . . . . 7 class (coe1𝑓)
1714, 16cfv 6110 . . . . . 6 class ((coe1𝑓)‘(( deg1𝑟)‘𝑓))
18 cui 18860 . . . . . . 7 class Unit
196, 18cfv 6110 . . . . . 6 class (Unit‘𝑟)
2017, 19wcel 2157 . . . . 5 wff ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) ∈ (Unit‘𝑟)
2111, 20wa 384 . . . 4 wff (𝑓 ≠ (0g‘(Poly1𝑟)) ∧ ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22 cbs 16087 . . . . 5 class Base
238, 22cfv 6110 . . . 4 class (Base‘(Poly1𝑟))
2421, 4, 23crab 3111 . . 3 class {𝑓 ∈ (Base‘(Poly1𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1𝑟)) ∧ ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
252, 3, 24cmpt 4934 . 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1𝑟)) ∧ ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
261, 25wceq 1637 1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1𝑟)) ∧ ((coe1𝑓)‘(( deg1𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
Colors of variables: wff setvar class
This definition is referenced by:  uc1pval  24135
  Copyright terms: Public domain W3C validator