Definition df-uc1p

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 . (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Assertion	df-uc1p	⊢ Unic1p = ( 𝑟 ∈ V ↦ { 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝑟 ) ) ∣ ( 𝑓 ≠ ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) ∈ ( Unit ‘ 𝑟 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuc1p	⊢ Unic1p
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		cui	⊢ Unit
20	6 19	cfv	⊢ ( Unit ‘ 𝑟 )
21	18 20	wcel	⊢ ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) ∈ ( Unit ‘ 𝑟 )
22	12 21	wa	⊢ ( 𝑓 ≠ ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) ∈ ( Unit ‘ 𝑟 ) )
23	22 3 8	crab	⊢ { 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝑟 ) ) ∣ ( 𝑓 ≠ ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) ∈ ( Unit ‘ 𝑟 ) ) }
24	1 2 23	cmpt	⊢ ( 𝑟 ∈ V ↦ { 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝑟 ) ) ∣ ( 𝑓 ≠ ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) ∈ ( Unit ‘ 𝑟 ) ) } )
25	0 24	wceq	⊢ Unic1p = ( 𝑟 ∈ V ↦ { 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝑟 ) ) ∣ ( 𝑓 ≠ ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) ∈ ( Unit ‘ 𝑟 ) ) } )