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 25873
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 25879. (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 25868 . 2 class Unic1p
2 vr . . 3 setvar π‘Ÿ
3 cvv 3474 . . 3 class V
4 vf . . . . . . 7 setvar 𝑓
54cv 1540 . . . . . 6 class 𝑓
62cv 1540 . . . . . . . 8 class π‘Ÿ
7 cpl1 21920 . . . . . . . 8 class Poly1
86, 7cfv 6543 . . . . . . 7 class (Poly1β€˜π‘Ÿ)
9 c0g 17389 . . . . . . 7 class 0g
108, 9cfv 6543 . . . . . 6 class (0gβ€˜(Poly1β€˜π‘Ÿ))
115, 10wne 2940 . . . . 5 wff 𝑓 β‰  (0gβ€˜(Poly1β€˜π‘Ÿ))
12 cdg1 25793 . . . . . . . . 9 class deg1
136, 12cfv 6543 . . . . . . . 8 class ( deg1 β€˜π‘Ÿ)
145, 13cfv 6543 . . . . . . 7 class (( deg1 β€˜π‘Ÿ)β€˜π‘“)
15 cco1 21921 . . . . . . . 8 class coe1
165, 15cfv 6543 . . . . . . 7 class (coe1β€˜π‘“)
1714, 16cfv 6543 . . . . . 6 class ((coe1β€˜π‘“)β€˜(( deg1 β€˜π‘Ÿ)β€˜π‘“))
18 cui 20246 . . . . . . 7 class Unit
196, 18cfv 6543 . . . . . 6 class (Unitβ€˜π‘Ÿ)
2017, 19wcel 2106 . . . . 5 wff ((coe1β€˜π‘“)β€˜(( deg1 β€˜π‘Ÿ)β€˜π‘“)) ∈ (Unitβ€˜π‘Ÿ)
2111, 20wa 396 . . . 4 wff (𝑓 β‰  (0gβ€˜(Poly1β€˜π‘Ÿ)) ∧ ((coe1β€˜π‘“)β€˜(( deg1 β€˜π‘Ÿ)β€˜π‘“)) ∈ (Unitβ€˜π‘Ÿ))
22 cbs 17148 . . . . 5 class Base
238, 22cfv 6543 . . . 4 class (Baseβ€˜(Poly1β€˜π‘Ÿ))
2421, 4, 23crab 3432 . . 3 class {𝑓 ∈ (Baseβ€˜(Poly1β€˜π‘Ÿ)) ∣ (𝑓 β‰  (0gβ€˜(Poly1β€˜π‘Ÿ)) ∧ ((coe1β€˜π‘“)β€˜(( deg1 β€˜π‘Ÿ)β€˜π‘“)) ∈ (Unitβ€˜π‘Ÿ))}
252, 3, 24cmpt 5231 . 2 class (π‘Ÿ ∈ V ↦ {𝑓 ∈ (Baseβ€˜(Poly1β€˜π‘Ÿ)) ∣ (𝑓 β‰  (0gβ€˜(Poly1β€˜π‘Ÿ)) ∧ ((coe1β€˜π‘“)β€˜(( deg1 β€˜π‘Ÿ)β€˜π‘“)) ∈ (Unitβ€˜π‘Ÿ))})
261, 25wceq 1541 1 wff Unic1p = (π‘Ÿ ∈ V ↦ {𝑓 ∈ (Baseβ€˜(Poly1β€˜π‘Ÿ)) ∣ (𝑓 β‰  (0gβ€˜(Poly1β€˜π‘Ÿ)) ∧ ((coe1β€˜π‘“)β€˜(( deg1 β€˜π‘Ÿ)β€˜π‘“)) ∈ (Unitβ€˜π‘Ÿ))})
Colors of variables: wff setvar class
This definition is referenced by:  uc1pval  25881
  Copyright terms: Public domain W3C validator