| Step |
Hyp |
Ref |
Expression |
| 1 |
|
noel |
|- -. a e. (/) |
| 2 |
|
noel |
|- -. ( a ` ( 1o X. { 0 } ) ) e. (/) |
| 3 |
|
eqid |
|- ( Poly1 ` (/) ) = ( Poly1 ` (/) ) |
| 4 |
|
eqid |
|- ( Base ` ( Poly1 ` (/) ) ) = ( Base ` ( Poly1 ` (/) ) ) |
| 5 |
|
base0 |
|- (/) = ( Base ` (/) ) |
| 6 |
3 4 5
|
ply1basf |
|- ( a e. ( Base ` ( Poly1 ` (/) ) ) -> a : ( NN0 ^m 1o ) --> (/) ) |
| 7 |
|
0nn0 |
|- 0 e. NN0 |
| 8 |
7
|
fconst6 |
|- ( 1o X. { 0 } ) : 1o --> NN0 |
| 9 |
|
nn0ex |
|- NN0 e. _V |
| 10 |
|
1oex |
|- 1o e. _V |
| 11 |
9 10
|
elmap |
|- ( ( 1o X. { 0 } ) e. ( NN0 ^m 1o ) <-> ( 1o X. { 0 } ) : 1o --> NN0 ) |
| 12 |
8 11
|
mpbir |
|- ( 1o X. { 0 } ) e. ( NN0 ^m 1o ) |
| 13 |
|
ffvelrn |
|- ( ( a : ( NN0 ^m 1o ) --> (/) /\ ( 1o X. { 0 } ) e. ( NN0 ^m 1o ) ) -> ( a ` ( 1o X. { 0 } ) ) e. (/) ) |
| 14 |
6 12 13
|
sylancl |
|- ( a e. ( Base ` ( Poly1 ` (/) ) ) -> ( a ` ( 1o X. { 0 } ) ) e. (/) ) |
| 15 |
2 14
|
mto |
|- -. a e. ( Base ` ( Poly1 ` (/) ) ) |
| 16 |
1 15
|
2false |
|- ( a e. (/) <-> a e. ( Base ` ( Poly1 ` (/) ) ) ) |
| 17 |
16
|
eqriv |
|- (/) = ( Base ` ( Poly1 ` (/) ) ) |