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