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

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 ⊢ 𝐴 = ( 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 11 12 4 13 mplelsfi ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 finSupp 0 )
15 5 6 7 8 mapsnf1o2 ⊢ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0
16 f1ocnv ⊢ ( ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0 → ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ℕ0 –1-1-onto→ ( ℕ0 ↑m 1o ) )
17 f1of1 ⊢ ( ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ℕ0 –1-1-onto→ ( ℕ0 ↑m 1o ) → ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ℕ0 –1-1→ ( ℕ0 ↑m 1o ) )
18 15 16 17 mp2b ⊢ ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ℕ0 –1-1→ ( ℕ0 ↑m 1o )
19 18 a1i ⊢ ( 𝐹 ∈ 𝐵 → ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ℕ0 –1-1→ ( ℕ0 ↑m 1o ) )
20 4 fvexi ⊢ 0 ∈ V
21 20 a1i ⊢ ( 𝐹 ∈ 𝐵 → 0 ∈ V )
22 id ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ 𝐵 )
23 14 19 21 22 fsuppco ⊢ ( 𝐹 ∈ 𝐵 → ( 𝐹 ∘ ◡ ( 𝑥 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) finSupp 0 )
24 10 23 eqbrtrd ⊢ ( 𝐹 ∈ 𝐵 → 𝐴 finSupp 0 )