Definition df-uc1p 26115

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 26121. (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 26110	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3431	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1546	. . . . . 6 class 𝑓
6	2	cv 1546	. . . . . . . 8 class 𝑟
7		cpl1 22162	. . . . . . . 8 class Poly1
8	6, 7	cfv 6485	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 17393	. . . . . . 7 class 0g
10	8, 9	cfv 6485	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2934	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 26037	. . . . . . . . 9 class deg1
13	6, 12	cfv 6485	. . . . . . . 8 class (deg1‘𝑟)
14	5, 13	cfv 6485	. . . . . . 7 class ((deg1‘𝑟)‘𝑓)
15		cco1 22163	. . . . . . . 8 class coe1
16	5, 15	cfv 6485	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6485	. . . . . 6 class ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓))
18		cui 20326	. . . . . . 7 class Unit
19	6, 18	cfv 6485	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2119	. . . . 5 wff ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 396	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 17170	. . . . 5 class Base
23	8, 22	cfv 6485	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3391	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5153	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1547	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is referenced by:  uc1pval  26123