Definition df-uc1p 25029

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 25035. (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 25024	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3408	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1542	. . . . . 6 class 𝑓
6	2	cv 1542	. . . . . . . 8 class 𝑟
7		cpl1 21098	. . . . . . . 8 class Poly1
8	6, 7	cfv 6380	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 16944	. . . . . . 7 class 0g
10	8, 9	cfv 6380	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2940	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 24949	. . . . . . . . 9 class deg1
13	6, 12	cfv 6380	. . . . . . . 8 class ( deg1 ‘𝑟)
14	5, 13	cfv 6380	. . . . . . 7 class (( deg1 ‘𝑟)‘𝑓)
15		cco1 21099	. . . . . . . 8 class coe1
16	5, 15	cfv 6380	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6380	. . . . . 6 class ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓))
18		cui 19657	. . . . . . 7 class Unit
19	6, 18	cfv 6380	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2110	. . . . 5 wff ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 399	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 16760	. . . . 5 class Base
23	8, 22	cfv 6380	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3065	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5135	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1543	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is referenced by:  uc1pval  25037