Definition df-mon1

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmn1	⊢ Monic1p
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vf	⊢ 𝑓
4		cbs	⊢ Base
5		cpl1	⊢ Poly1
6	1	cv	⊢ 𝑟
7	6 5	cfv	⊢ ( Poly1 ‘ 𝑟 )
8	7 4	cfv	⊢ ( Base ‘ ( Poly1 ‘ 𝑟 ) )
9	3	cv	⊢ 𝑓
10		c0g	⊢ 0g
11	7 10	cfv	⊢ ( 0g ‘ ( Poly1 ‘ 𝑟 ) )
12	9 11	wne	⊢ 𝑓 ≠ ( 0g ‘ ( Poly1 ‘ 𝑟 ) )
13		cco1	⊢ coe1
14	9 13	cfv	⊢ ( coe1 ‘ 𝑓 )
15		cdg1	⊢ deg1
16	6 15	cfv	⊢ ( deg1 ‘ 𝑟 )
17	9 16	cfv	⊢ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 )
18	17 14	cfv	⊢ ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) )
19		cur	⊢ 1r
20	6 19	cfv	⊢ ( 1r ‘ 𝑟 )
21	18 20	wceq	⊢ ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) = ( 1r ‘ 𝑟 )
22	12 21	wa	⊢ ( 𝑓 ≠ ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) = ( 1r ‘ 𝑟 ) )
23	22 3 8	crab	⊢ { 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝑟 ) ) ∣ ( 𝑓 ≠ ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) = ( 1r ‘ 𝑟 ) ) }
24	1 2 23	cmpt	⊢ ( 𝑟 ∈ V ↦ { 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝑟 ) ) ∣ ( 𝑓 ≠ ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) = ( 1r ‘ 𝑟 ) ) } )
25	0 24	wceq	⊢ Monic1p = ( 𝑟 ∈ V ↦ { 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝑟 ) ) ∣ ( 𝑓 ≠ ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) = ( 1r ‘ 𝑟 ) ) } )