# Metamath Proof Explorer

## Theorem coe1sfi

Description: Finite support of univariate polynomial coefficient vectors. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by AV, 19-Jul-2019)

Ref Expression
Hypotheses coe1sfi.a $⊢ A = coe 1 ⁡ F$
coe1sfi.b $⊢ B = Base P$
coe1sfi.p $⊢ P = Poly 1 ⁡ R$
coe1sfi.z
Assertion coe1sfi

### 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
5 df1o2 $⊢ 1 𝑜 = ∅$
6 nn0ex $⊢ ℕ 0 ∈ V$
7 0ex $⊢ ∅ ∈ V$
8 eqid $⊢ x ∈ ℕ 0 1 𝑜 ⟼ x ⁡ ∅ = x ∈ ℕ 0 1 𝑜 ⟼ x ⁡ ∅$
9 5 6 7 8 mapsncnv $⊢ x ∈ ℕ 0 1 𝑜 ⟼ x ⁡ ∅ -1 = y ∈ ℕ 0 ⟼ 1 𝑜 × y$
10 1 2 3 9 coe1fval2 $⊢ F ∈ B → A = F ∘ x ∈ ℕ 0 1 𝑜 ⟼ x ⁡ ∅ -1$
11 eqid $⊢ 1 𝑜 mPoly R = 1 𝑜 mPoly R$
12 eqid $⊢ Base 1 𝑜 mPoly R = Base 1 𝑜 mPoly R$
13 3 2 ply1bascl2 $⊢ F ∈ B → F ∈ Base 1 𝑜 mPoly R$
14 3 2 elbasfv $⊢ F ∈ B → R ∈ V$
15 11 12 4 13 14 mplelsfi
16 5 6 7 8 mapsnf1o2 $⊢ x ∈ ℕ 0 1 𝑜 ⟼ x ⁡ ∅ : ℕ 0 1 𝑜 ⟶ 1-1 onto ℕ 0$
17 f1ocnv $⊢ x ∈ ℕ 0 1 𝑜 ⟼ x ⁡ ∅ : ℕ 0 1 𝑜 ⟶ 1-1 onto ℕ 0 → x ∈ ℕ 0 1 𝑜 ⟼ x ⁡ ∅ -1 : ℕ 0 ⟶ 1-1 onto ℕ 0 1 𝑜$
18 f1of1 $⊢ x ∈ ℕ 0 1 𝑜 ⟼ x ⁡ ∅ -1 : ℕ 0 ⟶ 1-1 onto ℕ 0 1 𝑜 → x ∈ ℕ 0 1 𝑜 ⟼ x ⁡ ∅ -1 : ℕ 0 ⟶ 1-1 ℕ 0 1 𝑜$
19 16 17 18 mp2b $⊢ x ∈ ℕ 0 1 𝑜 ⟼ x ⁡ ∅ -1 : ℕ 0 ⟶ 1-1 ℕ 0 1 𝑜$
20 19 a1i $⊢ F ∈ B → x ∈ ℕ 0 1 𝑜 ⟼ x ⁡ ∅ -1 : ℕ 0 ⟶ 1-1 ℕ 0 1 𝑜$
21 4 fvexi
22 21 a1i
23 id $⊢ F ∈ B → F ∈ B$
24 15 20 22 23 fsuppco
25 10 24 eqbrtrd