Metamath Proof Explorer

Theorem coe1ae0

Description: The coefficient vector of a univariate polynomial is 0 almost everywhere. (Contributed by AV, 19-Oct-2019)

Ref Expression
Hypotheses coe1ae0.a 
|- A = ( coe1 ` F )
coe1ae0.b 
|- B = ( Base ` P )
coe1ae0.p 
|- P = ( Poly1 ` R )
coe1ae0.z 
|- .0. = ( 0g ` R )
Assertion coe1ae0 
|- ( F e. B -> E. s e. NN0 A. n e. NN0 ( s < n -> ( A ` n ) = .0. ) )

Proof

Step Hyp Ref Expression
1 coe1ae0.a 
 |-  A = ( coe1 ` F )
2 coe1ae0.b 
 |-  B = ( Base ` P )
3 coe1ae0.p 
 |-  P = ( Poly1 ` R )
4 coe1ae0.z 
 |-  .0. = ( 0g ` R )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 1 2 3 4 5 coe1fsupp 
 |-  ( F e. B -> A e. { a e. ( ( Base ` R ) ^m NN0 ) | a finSupp .0. } )
7 breq1 
 |-  ( a = A -> ( a finSupp .0. <-> A finSupp .0. ) )
8 7 elrab 
 |-  ( A e. { a e. ( ( Base ` R ) ^m NN0 ) | a finSupp .0. } <-> ( A e. ( ( Base ` R ) ^m NN0 ) /\ A finSupp .0. ) )
9 4 fvexi 
 |-  .0. e. _V
10 9 a1i 
 |-  ( F e. B -> .0. e. _V )
11 fsuppmapnn0ub 
 |-  ( ( A e. ( ( Base ` R ) ^m NN0 ) /\ .0. e. _V ) -> ( A finSupp .0. -> E. s e. NN0 A. n e. NN0 ( s < n -> ( A ` n ) = .0. ) ) )
12 10 11 sylan2 
 |-  ( ( A e. ( ( Base ` R ) ^m NN0 ) /\ F e. B ) -> ( A finSupp .0. -> E. s e. NN0 A. n e. NN0 ( s < n -> ( A ` n ) = .0. ) ) )
13 12 impancom 
 |-  ( ( A e. ( ( Base ` R ) ^m NN0 ) /\ A finSupp .0. ) -> ( F e. B -> E. s e. NN0 A. n e. NN0 ( s < n -> ( A ` n ) = .0. ) ) )
14 8 13 sylbi 
 |-  ( A e. { a e. ( ( Base ` R ) ^m NN0 ) | a finSupp .0. } -> ( F e. B -> E. s e. NN0 A. n e. NN0 ( s < n -> ( A ` n ) = .0. ) ) )
15 6 14 mpcom 
 |-  ( F e. B -> E. s e. NN0 A. n e. NN0 ( s < n -> ( A ` n ) = .0. ) )