Definition df-uc1p 26097

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 26103. (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 26092	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3429	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1541	. . . . . 6 class 𝑓
6	2	cv 1541	. . . . . . . 8 class 𝑟
7		cpl1 22140	. . . . . . . 8 class Poly1
8	6, 7	cfv 6498	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 17402	. . . . . . 7 class 0g
10	8, 9	cfv 6498	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2932	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 26019	. . . . . . . . 9 class deg1
13	6, 12	cfv 6498	. . . . . . . 8 class (deg1‘𝑟)
14	5, 13	cfv 6498	. . . . . . 7 class ((deg1‘𝑟)‘𝑓)
15		cco1 22141	. . . . . . . 8 class coe1
16	5, 15	cfv 6498	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6498	. . . . . 6 class ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓))
18		cui 20335	. . . . . . 7 class Unit
19	6, 18	cfv 6498	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2114	. . . . 5 wff ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 395	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 17179	. . . . 5 class Base
23	8, 22	cfv 6498	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3389	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5166	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1542	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is referenced by:  uc1pval  26105