Definition df-uc1p 25201

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 25207. (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 25196	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3422	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1538	. . . . . 6 class 𝑓
6	2	cv 1538	. . . . . . . 8 class 𝑟
7		cpl1 21258	. . . . . . . 8 class Poly1
8	6, 7	cfv 6418	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 17067	. . . . . . 7 class 0g
10	8, 9	cfv 6418	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2942	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 25121	. . . . . . . . 9 class deg1
13	6, 12	cfv 6418	. . . . . . . 8 class ( deg1 ‘𝑟)
14	5, 13	cfv 6418	. . . . . . 7 class (( deg1 ‘𝑟)‘𝑓)
15		cco1 21259	. . . . . . . 8 class coe1
16	5, 15	cfv 6418	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6418	. . . . . 6 class ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓))
18		cui 19796	. . . . . . 7 class Unit
19	6, 18	cfv 6418	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2108	. . . . 5 wff ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 395	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 16840	. . . . 5 class Base
23	8, 22	cfv 6418	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3067	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5153	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1539	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is referenced by:  uc1pval  25209