Definition df-uc1p 25649

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 25655. (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 25644	. 2 class Unic1p
2		vr	. . 3 setvar 𝑟
3		cvv 3475	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1541	. . . . . 6 class 𝑓
6	2	cv 1541	. . . . . . . 8 class 𝑟
7		cpl1 21701	. . . . . . . 8 class Poly1
8	6, 7	cfv 6544	. . . . . . 7 class (Poly1‘𝑟)
9		c0g 17385	. . . . . . 7 class 0g
10	8, 9	cfv 6544	. . . . . 6 class (0g‘(Poly1‘𝑟))
11	5, 10	wne 2941	. . . . 5 wff 𝑓 ≠ (0g‘(Poly1‘𝑟))
12		cdg1 25569	. . . . . . . . 9 class deg1
13	6, 12	cfv 6544	. . . . . . . 8 class ( deg1 ‘𝑟)
14	5, 13	cfv 6544	. . . . . . 7 class (( deg1 ‘𝑟)‘𝑓)
15		cco1 21702	. . . . . . . 8 class coe1
16	5, 15	cfv 6544	. . . . . . 7 class (coe1‘𝑓)
17	14, 16	cfv 6544	. . . . . 6 class ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓))
18		cui 20169	. . . . . . 7 class Unit
19	6, 18	cfv 6544	. . . . . 6 class (Unit‘𝑟)
20	17, 19	wcel 2107	. . . . 5 wff ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟)
21	11, 20	wa 397	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))
22		cbs 17144	. . . . 5 class Base
23	8, 22	cfv 6544	. . . 4 class (Base‘(Poly1‘𝑟))
24	21, 4, 23	crab 3433	. . 3 class {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}
25	2, 3, 24	cmpt 5232	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
26	1, 25	wceq 1542	1 wff Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})

This definition is referenced by:  uc1pval  25657