This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ˙