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	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
	coe1sfi.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	coe1sfi.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	coe1sfi.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	coe1sfi	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 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		df1o2	⊢ 1o = { ∅ }
6		nn0ex	⊢ ℕ0 ∈ V
7		0ex	⊢ ∅ ∈ V
8		eqid	⊢ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) = ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) )
9	5 6 7 8	mapsncnv	⊢ ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) = ( 𝑦 ∈ ℕ0 ↦ ( 1o × { 𝑦 } ) )
10	1 2 3 9	coe1fval2	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 = ( 𝐹 ∘ ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) )
11		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
12		eqid	⊢ ( Base ‘ ( 1o mPoly 𝑅 ) ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
13	3 2	ply1bascl2	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) )
14	3 2	elbasfv	⊢ ( 𝐹 ∈ 𝐵 → 𝑅 ∈ V )
15	11 12 4 13 14	mplelsfi	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 finSupp 0 )
16	5 6 7 8	mapsnf1o2	⊢ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0
17		f1ocnv	⊢ ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0 → ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ℕ0 –1-1-onto→ ( ℕ0 ↑m 1o ) )
18		f1of1	⊢ ( ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ℕ0 –1-1-onto→ ( ℕ0 ↑m 1o ) → ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ℕ0 –1-1→ ( ℕ0 ↑m 1o ) )
19	16 17 18	mp2b	⊢ ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ℕ0 –1-1→ ( ℕ0 ↑m 1o )
20	19	a1i	⊢ ( 𝐹 ∈ 𝐵 → ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ℕ0 –1-1→ ( ℕ0 ↑m 1o ) )
21	4	fvexi	⊢ 0 ∈ V
22	21	a1i	⊢ ( 𝐹 ∈ 𝐵 → 0 ∈ V )
23		id	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ 𝐵 )
24	15 20 22 23	fsuppco	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐹 ∘ ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) finSupp 0 )
25	10 24	eqbrtrd	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 finSupp 0 )