Definition df-uc1p 26070

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 26076. (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 26065	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3444	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1539	. . . . . 6 class 𝑓
6	2	cv 1539	. . . . . . . 8 class 𝑟
7		cpl1 22094	. . . . . . . 8 class Poly1
8	6, 7	cfv 6499	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 17378	. . . . . . 7 class 0g
10	8, 9	cfv 6499	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2925	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 25992	. . . . . . . . 9 class deg1
13	6, 12	cfv 6499	. . . . . . . 8 class (deg1‘𝑟)
14	5, 13	cfv 6499	. . . . . . 7 class ((deg1‘𝑟)‘𝑓)
15		cco1 22095	. . . . . . . 8 class coe1
16	5, 15	cfv 6499	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6499	. . . . . 6 class ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓))
18		cui 20275	. . . . . . 7 class Unit
19	6, 18	cfv 6499	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2109	. . . . 5 wff ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 395	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 17155	. . . . 5 class Base
23	8, 22	cfv 6499	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3402	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5183	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1540	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is referenced by:  uc1pval  26078