Definition df-uc1p 23891

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 23897. (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 23886	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3200	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1482	. . . . . 6 class 𝑓
6	2	cv 1482	. . . . . . . 8 class 𝑟
7		cpl1 19547	. . . . . . . 8 class Poly1
8	6, 7	cfv 5888	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 16100	. . . . . . 7 class 0g
10	8, 9	cfv 5888	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2794	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 23814	. . . . . . . . 9 class deg1
13	6, 12	cfv 5888	. . . . . . . 8 class ( deg1 ‘𝑟)
14	5, 13	cfv 5888	. . . . . . 7 class (( deg1 ‘𝑟)‘𝑓)
15		cco1 19548	. . . . . . . 8 class coe1
16	5, 15	cfv 5888	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 5888	. . . . . 6 class ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓))
18		cui 18639	. . . . . . 7 class Unit
19	6, 18	cfv 5888	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 1990	. . . . 5 wff ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 384	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 15857	. . . . 5 class Base
23	8, 22	cfv 5888	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 2916	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 4729	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1483	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is referenced by:  uc1pval  23899