Definition df-uc1p 26450

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 26456. (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 26445	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3451	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1569	. . . . . 6 class 𝑓
6	2	cv 1569	. . . . . . . 8 class 𝑟
7		cpl1 22495	. . . . . . . 8 class Poly1
8	6, 7	cfv 6538	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 17610	. . . . . . 7 class 0g
10	8, 9	cfv 6538	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2956	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 26372	. . . . . . . . 9 class deg1
13	6, 12	cfv 6538	. . . . . . . 8 class (deg1‘𝑟)
14	5, 13	cfv 6538	. . . . . . 7 class ((deg1‘𝑟)‘𝑓)
15		cco1 22496	. . . . . . . 8 class coe1
16	5, 15	cfv 6538	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6538	. . . . . 6 class ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓))
18		cui 20585	. . . . . . 7 class Unit
19	6, 18	cfv 6538	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2145	. . . . 5 wff ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 401	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 17387	. . . . 5 class Base
23	8, 22	cfv 6538	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3413	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5186	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1570	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is used by:  uc1pval  26458