Metamath Proof Explorer

Theorem mptcoe1fsupp

Description: A mapping involving coefficients of polynomials is finitely supported. (Contributed by AV, 12-Oct-2019)

Ref Expression
Hypotheses mptcoe1fsupp.p 
|- P = ( Poly1 ` R )
mptcoe1fsupp.b 
|- B = ( Base ` P )
mptcoe1fsupp.0 
|- .0. = ( 0g ` R )
Assertion mptcoe1fsupp 
|- ( ( R e. Ring /\ M e. B ) -> ( k e. NN0 |-> ( ( coe1 ` M ) ` k ) ) finSupp .0. )

Proof

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. )