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 = coe 1 F
coe1ae0.b B = Base P
coe1ae0.p P = Poly 1 R
coe1ae0.z 0 ˙ = 0 R
Assertion coe1ae0 F B s 0 n 0 s < n A n = 0 ˙

Proof

Step Hyp Ref Expression
1 coe1ae0.a A = coe 1 F
2 coe1ae0.b B = Base P
3 coe1ae0.p P = Poly 1 R
4 coe1ae0.z 0 ˙ = 0 R
5 eqid Base R = Base R
6 1 2 3 4 5 coe1fsupp F B A a Base R 0 | finSupp 0 ˙ a
7 breq1 a = A finSupp 0 ˙ a finSupp 0 ˙ A
8 7 elrab A a Base R 0 | finSupp 0 ˙ a A Base R 0 finSupp 0 ˙ A
9 4 fvexi 0 ˙ V
10 9 a1i F B 0 ˙ V
11 fsuppmapnn0ub A Base R 0 0 ˙ V finSupp 0 ˙ A s 0 n 0 s < n A n = 0 ˙
12 10 11 sylan2 A Base R 0 F B finSupp 0 ˙ A s 0 n 0 s < n A n = 0 ˙
13 12 impancom A Base R 0 finSupp 0 ˙ A F B s 0 n 0 s < n A n = 0 ˙
14 8 13 sylbi A a Base R 0 | finSupp 0 ˙ a F B s 0 n 0 s < n A n = 0 ˙
15 6 14 mpcom F B s 0 n 0 s < n A n = 0 ˙