Step |
Hyp |
Ref |
Expression |
1 |
|
coe1sfi.a |
|- A = ( coe1 ` F ) |
2 |
|
coe1sfi.b |
|- B = ( Base ` P ) |
3 |
|
coe1sfi.p |
|- P = ( Poly1 ` R ) |
4 |
|
coe1sfi.z |
|- .0. = ( 0g ` R ) |
5 |
|
coe1fvalcl.k |
|- K = ( Base ` R ) |
6 |
|
breq1 |
|- ( g = A -> ( g finSupp .0. <-> A finSupp .0. ) ) |
7 |
1 2 3 5
|
coe1f |
|- ( F e. B -> A : NN0 --> K ) |
8 |
5
|
fvexi |
|- K e. _V |
9 |
|
nn0ex |
|- NN0 e. _V |
10 |
8 9
|
pm3.2i |
|- ( K e. _V /\ NN0 e. _V ) |
11 |
|
elmapg |
|- ( ( K e. _V /\ NN0 e. _V ) -> ( A e. ( K ^m NN0 ) <-> A : NN0 --> K ) ) |
12 |
10 11
|
mp1i |
|- ( F e. B -> ( A e. ( K ^m NN0 ) <-> A : NN0 --> K ) ) |
13 |
7 12
|
mpbird |
|- ( F e. B -> A e. ( K ^m NN0 ) ) |
14 |
1 2 3 4
|
coe1sfi |
|- ( F e. B -> A finSupp .0. ) |
15 |
6 13 14
|
elrabd |
|- ( F e. B -> A e. { g e. ( K ^m NN0 ) | g finSupp .0. } ) |