Definition df-uc1p 26459

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 26465. (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 26454	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3450	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1568	. . . . . 6 class 𝑓
6	2	cv 1568	. . . . . . . 8 class 𝑟
7		cpl1 22504	. . . . . . . 8 class Poly1
8	6, 7	cfv 6543	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 17619	. . . . . . 7 class 0g
10	8, 9	cfv 6543	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2955	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 26381	. . . . . . . . 9 class deg1
13	6, 12	cfv 6543	. . . . . . . 8 class (deg1‘𝑟)
14	5, 13	cfv 6543	. . . . . . 7 class ((deg1‘𝑟)‘𝑓)
15		cco1 22505	. . . . . . . 8 class coe1
16	5, 15	cfv 6543	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6543	. . . . . 6 class ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓))
18		cui 20594	. . . . . . 7 class Unit
19	6, 18	cfv 6543	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2144	. . . . 5 wff ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 401	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 17396	. . . . 5 class Base
23	8, 22	cfv 6543	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3412	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5185	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1569	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is used by:  uc1pval  26467