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 } )