This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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