Definition df-uc1p 26192

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 26198. (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 26187	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3454	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1559	. . . . . 6 class 𝑓
6	2	cv 1559	. . . . . . . 8 class 𝑟
7		cpl1 22239	. . . . . . . 8 class Poly1
8	6, 7	cfv 6521	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 17468	. . . . . . 7 class 0g
10	8, 9	cfv 6521	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2957	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 26114	. . . . . . . . 9 class deg1
13	6, 12	cfv 6521	. . . . . . . 8 class (deg1‘𝑟)
14	5, 13	cfv 6521	. . . . . . 7 class ((deg1‘𝑟)‘𝑓)
15		cco1 22240	. . . . . . . 8 class coe1
16	5, 15	cfv 6521	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6521	. . . . . 6 class ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓))
18		cui 20404	. . . . . . 7 class Unit
19	6, 18	cfv 6521	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2142	. . . . 5 wff ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 399	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 17245	. . . . 5 class Base
23	8, 22	cfv 6521	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3414	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5181	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1560	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is referenced by:  uc1pval  26200