Step |
Hyp |
Ref |
Expression |
1 |
|
mptcoe1fsupp.p |
|- P = ( Poly1 ` R ) |
2 |
|
mptcoe1fsupp.b |
|- B = ( Base ` P ) |
3 |
|
mptcoe1fsupp.0 |
|- .0. = ( 0g ` R ) |
4 |
3
|
fvexi |
|- .0. e. _V |
5 |
4
|
a1i |
|- ( ( R e. Ring /\ M e. B ) -> .0. e. _V ) |
6 |
|
eqid |
|- ( coe1 ` M ) = ( coe1 ` M ) |
7 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
8 |
6 2 1 7
|
coe1fvalcl |
|- ( ( M e. B /\ k e. NN0 ) -> ( ( coe1 ` M ) ` k ) e. ( Base ` R ) ) |
9 |
8
|
adantll |
|- ( ( ( R e. Ring /\ M e. B ) /\ k e. NN0 ) -> ( ( coe1 ` M ) ` k ) e. ( Base ` R ) ) |
10 |
|
simpr |
|- ( ( R e. Ring /\ M e. B ) -> M e. B ) |
11 |
6 2 1 3 7
|
coe1fsupp |
|- ( M e. B -> ( coe1 ` M ) e. { c e. ( ( Base ` R ) ^m NN0 ) | c finSupp .0. } ) |
12 |
|
elrabi |
|- ( ( coe1 ` M ) e. { c e. ( ( Base ` R ) ^m NN0 ) | c finSupp .0. } -> ( coe1 ` M ) e. ( ( Base ` R ) ^m NN0 ) ) |
13 |
10 11 12
|
3syl |
|- ( ( R e. Ring /\ M e. B ) -> ( coe1 ` M ) e. ( ( Base ` R ) ^m NN0 ) ) |
14 |
13 4
|
jctir |
|- ( ( R e. Ring /\ M e. B ) -> ( ( coe1 ` M ) e. ( ( Base ` R ) ^m NN0 ) /\ .0. e. _V ) ) |
15 |
6 2 1 3
|
coe1sfi |
|- ( M e. B -> ( coe1 ` M ) finSupp .0. ) |
16 |
15
|
adantl |
|- ( ( R e. Ring /\ M e. B ) -> ( coe1 ` M ) finSupp .0. ) |
17 |
|
fsuppmapnn0ub |
|- ( ( ( coe1 ` M ) e. ( ( Base ` R ) ^m NN0 ) /\ .0. e. _V ) -> ( ( coe1 ` M ) finSupp .0. -> E. s e. NN0 A. x e. NN0 ( s < x -> ( ( coe1 ` M ) ` x ) = .0. ) ) ) |
18 |
14 16 17
|
sylc |
|- ( ( R e. Ring /\ M e. B ) -> E. s e. NN0 A. x e. NN0 ( s < x -> ( ( coe1 ` M ) ` x ) = .0. ) ) |
19 |
|
csbfv |
|- [_ x / k ]_ ( ( coe1 ` M ) ` k ) = ( ( coe1 ` M ) ` x ) |
20 |
|
simpr |
|- ( ( ( ( ( ( R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) /\ s < x ) /\ ( ( coe1 ` M ) ` x ) = .0. ) -> ( ( coe1 ` M ) ` x ) = .0. ) |
21 |
19 20
|
syl5eq |
|- ( ( ( ( ( ( R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) /\ s < x ) /\ ( ( coe1 ` M ) ` x ) = .0. ) -> [_ x / k ]_ ( ( coe1 ` M ) ` k ) = .0. ) |
22 |
21
|
exp31 |
|- ( ( ( ( R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) -> ( s < x -> ( ( ( coe1 ` M ) ` x ) = .0. -> [_ x / k ]_ ( ( coe1 ` M ) ` k ) = .0. ) ) ) |
23 |
22
|
a2d |
|- ( ( ( ( R e. Ring /\ M e. B ) /\ s e. NN0 ) /\ x e. NN0 ) -> ( ( s < x -> ( ( coe1 ` M ) ` x ) = .0. ) -> ( s < x -> [_ x / k ]_ ( ( coe1 ` M ) ` k ) = .0. ) ) ) |
24 |
23
|
ralimdva |
|- ( ( ( R e. Ring /\ M e. B ) /\ s e. NN0 ) -> ( A. x e. NN0 ( s < x -> ( ( coe1 ` M ) ` x ) = .0. ) -> A. x e. NN0 ( s < x -> [_ x / k ]_ ( ( coe1 ` M ) ` k ) = .0. ) ) ) |
25 |
24
|
reximdva |
|- ( ( R e. Ring /\ M e. B ) -> ( E. s e. NN0 A. x e. NN0 ( s < x -> ( ( coe1 ` M ) ` x ) = .0. ) -> E. s e. NN0 A. x e. NN0 ( s < x -> [_ x / k ]_ ( ( coe1 ` M ) ` k ) = .0. ) ) ) |
26 |
18 25
|
mpd |
|- ( ( R e. Ring /\ M e. B ) -> E. s e. NN0 A. x e. NN0 ( s < x -> [_ x / k ]_ ( ( coe1 ` M ) ` k ) = .0. ) ) |
27 |
5 9 26
|
mptnn0fsupp |
|- ( ( R e. Ring /\ M e. B ) -> ( k e. NN0 |-> ( ( coe1 ` M ) ` k ) ) finSupp .0. ) |