Metamath Proof Explorer


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𝑟 ) ) } )