Metamath Proof Explorer


Theorem coe1fsupp

Description: The coefficient vector of a univariate polynomial is a finitely supported mapping from the nonnegative integers to the elements of the coefficient class/ring for the polynomial. (Contributed by AV, 3-Oct-2019)

Ref Expression
Hypotheses coe1sfi.a A = coe 1 F
coe1sfi.b B = Base P
coe1sfi.p P = Poly 1 R
coe1sfi.z 0 ˙ = 0 R
coe1fvalcl.k K = Base R
Assertion coe1fsupp F B A g K 0 | finSupp 0 ˙ g

Proof

Step Hyp Ref Expression
1 coe1sfi.a A = coe 1 F
2 coe1sfi.b B = Base P
3 coe1sfi.p P = Poly 1 R
4 coe1sfi.z 0 ˙ = 0 R
5 coe1fvalcl.k K = Base R
6 breq1 g = A finSupp 0 ˙ g finSupp 0 ˙ A
7 1 2 3 5 coe1f F B A : 0 K
8 5 fvexi K V
9 nn0ex 0 V
10 8 9 pm3.2i K V 0 V
11 elmapg K V 0 V A K 0 A : 0 K
12 10 11 mp1i F B A K 0 A : 0 K
13 7 12 mpbird F B A K 0
14 1 2 3 4 coe1sfi F B finSupp 0 ˙ A
15 6 13 14 elrabd F B A g K 0 | finSupp 0 ˙ g