Definition df-uc1p 26289

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 26295. (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 26284	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3455	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1569	. . . . . 6 class 𝑓
6	2	cv 1569	. . . . . . . 8 class 𝑟
7		cpl1 22337	. . . . . . . 8 class Poly1
8	6, 7	cfv 6536	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 17487	. . . . . . 7 class 0g
10	8, 9	cfv 6536	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2958	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 26211	. . . . . . . . 9 class deg1
13	6, 12	cfv 6536	. . . . . . . 8 class (deg1‘𝑟)
14	5, 13	cfv 6536	. . . . . . 7 class ((deg1‘𝑟)‘𝑓)
15		cco1 22338	. . . . . . . 8 class coe1
16	5, 15	cfv 6536	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6536	. . . . . 6 class ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓))
18		cui 20433	. . . . . . 7 class Unit
19	6, 18	cfv 6536	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2143	. . . . 5 wff ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 400	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 17264	. . . . 5 class Base
23	8, 22	cfv 6536	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3416	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5192	. 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 referenced by:  uc1pval  26297