Definition df-uc1p 24408

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 24414. (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 24403	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3436	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1521	. . . . . 6 class 𝑓
6	2	cv 1521	. . . . . . . 8 class 𝑟
7		cpl1 20028	. . . . . . . 8 class Poly1
8	6, 7	cfv 6228	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 16542	. . . . . . 7 class 0g
10	8, 9	cfv 6228	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2983	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 24331	. . . . . . . . 9 class deg1
13	6, 12	cfv 6228	. . . . . . . 8 class ( deg1 ‘𝑟)
14	5, 13	cfv 6228	. . . . . . 7 class (( deg1 ‘𝑟)‘𝑓)
15		cco1 20029	. . . . . . . 8 class coe1
16	5, 15	cfv 6228	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6228	. . . . . 6 class ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓))
18		cui 19079	. . . . . . 7 class Unit
19	6, 18	cfv 6228	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2080	. . . . 5 wff ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 396	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 16312	. . . . 5 class Base
23	8, 22	cfv 6228	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3108	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5043	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1522	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is referenced by:  uc1pval  24416