Definition df-uc1p 26091

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 26097. (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 26086	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3438	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1540	. . . . . 6 class 𝑓
6	2	cv 1540	. . . . . . . 8 class 𝑟
7		cpl1 22115	. . . . . . . 8 class Poly1
8	6, 7	cfv 6490	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 17357	. . . . . . 7 class 0g
10	8, 9	cfv 6490	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2930	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 26013	. . . . . . . . 9 class deg1
13	6, 12	cfv 6490	. . . . . . . 8 class (deg1‘𝑟)
14	5, 13	cfv 6490	. . . . . . 7 class ((deg1‘𝑟)‘𝑓)
15		cco1 22116	. . . . . . . 8 class coe1
16	5, 15	cfv 6490	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6490	. . . . . 6 class ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓))
18		cui 20289	. . . . . . 7 class Unit
19	6, 18	cfv 6490	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2113	. . . . 5 wff ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 395	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 17134	. . . . 5 class Base
23	8, 22	cfv 6490	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3397	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5177	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1541	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is referenced by:  uc1pval  26099