| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fvi |
|- ( R e. _V -> ( _I ` R ) = R ) |
| 2 |
1
|
fveq2d |
|- ( R e. _V -> ( deg1 ` ( _I ` R ) ) = ( deg1 ` R ) ) |
| 3 |
|
eqid |
|- ( deg1 ` (/) ) = ( deg1 ` (/) ) |
| 4 |
|
eqid |
|- ( Poly1 ` (/) ) = ( Poly1 ` (/) ) |
| 5 |
|
00ply1bas |
|- (/) = ( Base ` ( Poly1 ` (/) ) ) |
| 6 |
3 4 5
|
deg1xrf |
|- ( deg1 ` (/) ) : (/) --> RR* |
| 7 |
|
ffn |
|- ( ( deg1 ` (/) ) : (/) --> RR* -> ( deg1 ` (/) ) Fn (/) ) |
| 8 |
6 7
|
ax-mp |
|- ( deg1 ` (/) ) Fn (/) |
| 9 |
|
fn0 |
|- ( ( deg1 ` (/) ) Fn (/) <-> ( deg1 ` (/) ) = (/) ) |
| 10 |
8 9
|
mpbi |
|- ( deg1 ` (/) ) = (/) |
| 11 |
|
fvprc |
|- ( -. R e. _V -> ( _I ` R ) = (/) ) |
| 12 |
11
|
fveq2d |
|- ( -. R e. _V -> ( deg1 ` ( _I ` R ) ) = ( deg1 ` (/) ) ) |
| 13 |
|
fvprc |
|- ( -. R e. _V -> ( deg1 ` R ) = (/) ) |
| 14 |
10 12 13
|
3eqtr4a |
|- ( -. R e. _V -> ( deg1 ` ( _I ` R ) ) = ( deg1 ` R ) ) |
| 15 |
2 14
|
pm2.61i |
|- ( deg1 ` ( _I ` R ) ) = ( deg1 ` R ) |
| 16 |
15
|
eqcomi |
|- ( deg1 ` R ) = ( deg1 ` ( _I ` R ) ) |