Definition df-uc1p 26191

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 26197. (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 26186	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3488	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1536	. . . . . 6 class 𝑓
6	2	cv 1536	. . . . . . . 8 class 𝑟
7		cpl1 22199	. . . . . . . 8 class Poly1
8	6, 7	cfv 6573	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 17499	. . . . . . 7 class 0g
10	8, 9	cfv 6573	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2946	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 26113	. . . . . . . . 9 class deg1
13	6, 12	cfv 6573	. . . . . . . 8 class (deg1‘𝑟)
14	5, 13	cfv 6573	. . . . . . 7 class ((deg1‘𝑟)‘𝑓)
15		cco1 22200	. . . . . . . 8 class coe1
16	5, 15	cfv 6573	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6573	. . . . . 6 class ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓))
18		cui 20381	. . . . . . 7 class Unit
19	6, 18	cfv 6573	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2108	. . . . 5 wff ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 395	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 17258	. . . . 5 class Base
23	8, 22	cfv 6573	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3443	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5249	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1537	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is referenced by:  uc1pval  26199