Definition df-uc1p 24725

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 24731. (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 24720	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3494	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1536	. . . . . 6 class 𝑓
6	2	cv 1536	. . . . . . . 8 class 𝑟
7		cpl1 20345	. . . . . . . 8 class Poly1
8	6, 7	cfv 6355	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 16713	. . . . . . 7 class 0g
10	8, 9	cfv 6355	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 3016	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 24648	. . . . . . . . 9 class deg1
13	6, 12	cfv 6355	. . . . . . . 8 class ( deg1 ‘𝑟)
14	5, 13	cfv 6355	. . . . . . 7 class (( deg1 ‘𝑟)‘𝑓)
15		cco1 20346	. . . . . . . 8 class coe1
16	5, 15	cfv 6355	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6355	. . . . . 6 class ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓))
18		cui 19389	. . . . . . 7 class Unit
19	6, 18	cfv 6355	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2114	. . . . 5 wff ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 398	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 16483	. . . . 5 class Base
23	8, 22	cfv 6355	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3142	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5146	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1537	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is referenced by:  uc1pval  24733