Definition df-mon1 25200

Description: Define the set of monic univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)

Assertion

Ref	Expression
df-mon1	⊢ Monic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) = (1r‘𝑟))})

Distinct variable group:   𝑓,𝑟

Detailed syntax breakdown of Definition df-mon1

Step	Hyp	Ref	Expression
1		cmn1 25195	. 2 class Monic1p
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		cur 19652	. . . . . . 7 class 1r
19	6, 18	cfv 6418	. . . . . 6 class (1r‘𝑟)
20	17, 19	wceq 1539	. . . . 5 wff ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) = (1r‘𝑟)
21	11, 20	wa 395	. . . 4 wff (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) = (1r‘𝑟))
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 ‘𝑟)‘𝑓)) = (1r‘𝑟))}
25	2, 3, 24	cmpt 5153	. 2 class (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) = (1r‘𝑟))})
26	1, 25	wceq 1539	1 wff Monic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) = (1r‘𝑟))})

This definition is referenced by:  mon1pval  25211