Definition df-uc1p 26257

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 26263. (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 26252	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3463	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1566	. . . . . 6 class 𝑓
6	2	cv 1566	. . . . . . . 8 class 𝑟
7		cpl1 22305	. . . . . . . 8 class Poly1
8	6, 7	cfv 6537	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 17491	. . . . . . 7 class 0g
10	8, 9	cfv 6537	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2964	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 26179	. . . . . . . . 9 class deg1
13	6, 12	cfv 6537	. . . . . . . 8 class (deg1‘𝑟)
14	5, 13	cfv 6537	. . . . . . 7 class ((deg1‘𝑟)‘𝑓)
15		cco1 22306	. . . . . . . 8 class coe1
16	5, 15	cfv 6537	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6537	. . . . . 6 class ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓))
18		cui 20436	. . . . . . 7 class Unit
19	6, 18	cfv 6537	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2149	. . . . 5 wff ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 400	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 17268	. . . . 5 class Base
23	8, 22	cfv 6537	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3423	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5196	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1567	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is referenced by:  uc1pval  26265