Step |
Hyp |
Ref |
Expression |
0 |
|
cmn1 |
|- Monic1p |
1 |
|
vr |
|- r |
2 |
|
cvv |
|- _V |
3 |
|
vf |
|- f |
4 |
|
cbs |
|- Base |
5 |
|
cpl1 |
|- Poly1 |
6 |
1
|
cv |
|- r |
7 |
6 5
|
cfv |
|- ( Poly1 ` r ) |
8 |
7 4
|
cfv |
|- ( Base ` ( Poly1 ` r ) ) |
9 |
3
|
cv |
|- f |
10 |
|
c0g |
|- 0g |
11 |
7 10
|
cfv |
|- ( 0g ` ( Poly1 ` r ) ) |
12 |
9 11
|
wne |
|- f =/= ( 0g ` ( Poly1 ` r ) ) |
13 |
|
cco1 |
|- coe1 |
14 |
9 13
|
cfv |
|- ( coe1 ` f ) |
15 |
|
cdg1 |
|- deg1 |
16 |
6 15
|
cfv |
|- ( deg1 ` r ) |
17 |
9 16
|
cfv |
|- ( ( deg1 ` r ) ` f ) |
18 |
17 14
|
cfv |
|- ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) |
19 |
|
cur |
|- 1r |
20 |
6 19
|
cfv |
|- ( 1r ` r ) |
21 |
18 20
|
wceq |
|- ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) |
22 |
12 21
|
wa |
|- ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) |
23 |
22 3 8
|
crab |
|- { f e. ( Base ` ( Poly1 ` r ) ) | ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) } |
24 |
1 2 23
|
cmpt |
|- ( r e. _V |-> { f e. ( Base ` ( Poly1 ` r ) ) | ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) } ) |
25 |
0 24
|
wceq |
|- Monic1p = ( r e. _V |-> { f e. ( Base ` ( Poly1 ` r ) ) | ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) } ) |