Definition df-uc1p 23695

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 23701. (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 23690	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3173	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1474	. . . . . 6 class 𝑓
6	2	cv 1474	. . . . . . . 8 class 𝑟
7		cpl1 19368	. . . . . . . 8 class Poly1
8	6, 7	cfv 5804	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 15923	. . . . . . 7 class 0g
10	8, 9	cfv 5804	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2780	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 23618	. . . . . . . . 9 class deg1
13	6, 12	cfv 5804	. . . . . . . 8 class ( deg1 ‘𝑟)
14	5, 13	cfv 5804	. . . . . . 7 class (( deg1 ‘𝑟)‘𝑓)
15		cco1 19369	. . . . . . . 8 class coe1
16	5, 15	cfv 5804	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 5804	. . . . . 6 class ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓))
18		cui 18462	. . . . . . 7 class Unit
19	6, 18	cfv 5804	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 1977	. . . . 5 wff ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 383	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 15695	. . . . 5 class Base
23	8, 22	cfv 5804	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 2900	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 4643	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1475	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is referenced by:  uc1pval  23703