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

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 ⊢ 𝐴 = ( coe1 ‘ 𝐹 )
coe1sfi.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
coe1sfi.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
coe1sfi.z ⊢ 0 = ( 0g ‘ 𝑅 )
coe1fvalcl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
Assertion coe1fsupp ( 𝐹 ∈ 𝐵 → 𝐴 ∈ { 𝑔 ∈ ( 𝐾 ↑m ℕ0 ) ∣ 𝑔 finSupp 0 } )

Proof

Step Hyp Ref Expression
1 coe1sfi.a ⊢ 𝐴 = ( coe1 ‘ 𝐹 )
2 coe1sfi.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 coe1sfi.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 coe1sfi.z ⊢ 0 = ( 0g ‘ 𝑅 )
5 coe1fvalcl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
6 breq1 ⊢ ( 𝑔 = 𝐴 → ( 𝑔 finSupp 0 ↔ 𝐴 finSupp 0 ) )
7 1 2 3 5 coe1f ⊢ ( 𝐹 ∈ 𝐵 → 𝐴 : ℕ0 ⟶ 𝐾 )
8 5 fvexi ⊢ 𝐾 ∈ V
9 nn0ex ⊢ ℕ0 ∈ V
10 8 9 pm3.2i ⊢ ( 𝐾 ∈ V ∧ ℕ0 ∈ V )
11 elmapg ⊢ ( ( 𝐾 ∈ V ∧ ℕ0 ∈ V ) → ( 𝐴 ∈ ( 𝐾 ↑m ℕ0 ) ↔ 𝐴 : ℕ0 ⟶ 𝐾 ) )
12 10 11 mp1i ⊢ ( 𝐹 ∈ 𝐵 → ( 𝐴 ∈ ( 𝐾 ↑m ℕ0 ) ↔ 𝐴 : ℕ0 ⟶ 𝐾 ) )
13 7 12 mpbird ⊢ ( 𝐹 ∈ 𝐵 → 𝐴 ∈ ( 𝐾 ↑m ℕ0 ) )
14 1 2 3 4 coe1sfi ⊢ ( 𝐹 ∈ 𝐵 → 𝐴 finSupp 0 )
15 6 13 14 elrabd ⊢ ( 𝐹 ∈ 𝐵 → 𝐴 ∈ { 𝑔 ∈ ( 𝐾 ↑m ℕ0 ) ∣ 𝑔 finSupp 0 } )