Definition df-uc1p 26342

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 26348. (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

Step	Hyp	Ref	Expression
1		cuc1p 26337	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3457	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1569	. . . . . 6 class 𝑓
6	2	cv 1569	. . . . . . . 8 class 𝑟
7		cpl1 22389	. . . . . . . 8 class Poly1
8	6, 7	cfv 6540	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 17516	. . . . . . 7 class 0g
10	8, 9	cfv 6540	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2960	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 26264	. . . . . . . . 9 class deg1
13	6, 12	cfv 6540	. . . . . . . 8 class (deg1‘𝑟)
14	5, 13	cfv 6540	. . . . . . 7 class ((deg1‘𝑟)‘𝑓)
15		cco1 22390	. . . . . . . 8 class coe1
16	5, 15	cfv 6540	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6540	. . . . . 6 class ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓))
18		cui 20485	. . . . . . 7 class Unit
19	6, 18	cfv 6540	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2146	. . . . 5 wff ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 401	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 17293	. . . . 5 class Base
23	8, 22	cfv 6540	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3418	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5194	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1570	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is used by:  uc1pval  26350