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	$⊢ A = {coe}_{1} (F)$
		coe1sfi.b	$⊢ B = {Base}_{P}$
		coe1sfi.p	$⊢ P = {Poly}_{1} (R)$
		coe1sfi.z	$⊢ \underset{˙}{0} = 0_{R}$
		coe1fvalcl.k	$⊢ K = {Base}_{R}$
	Assertion	coe1fsupp	$⊢ F \in B \to A \in \{g \in (K^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (g)\}$

Proof

Step	Hyp	Ref	Expression
1		coe1sfi.a	$⊢ A = {coe}_{1} (F)$
2		coe1sfi.b	$⊢ B = {Base}_{P}$
3		coe1sfi.p	$⊢ P = {Poly}_{1} (R)$
4		coe1sfi.z	$⊢ \underset{˙}{0} = 0_{R}$
5		coe1fvalcl.k	$⊢ K = {Base}_{R}$
6		breq1	$⊢ g = A \to ({finSupp}_{\underset{˙}{0}} (g) \leftrightarrow {finSupp}_{\underset{˙}{0}} (A))$
7	1 2 3 5	coe1f	$⊢ F \in B \to A : ℕ_{0} ⟶ K$
8	5	fvexi	$⊢ K \in V$
9		nn0ex	$⊢ ℕ_{0} \in V$
10	8 9	pm3.2i	$⊢ (K \in V \land ℕ_{0} \in V)$
11		elmapg	$⊢ (K \in V \land ℕ_{0} \in V) \to (A \in (K^{ℕ_{0}}) \leftrightarrow A : ℕ_{0} ⟶ K)$
12	10 11	mp1i	$⊢ F \in B \to (A \in (K^{ℕ_{0}}) \leftrightarrow A : ℕ_{0} ⟶ K)$
13	7 12	mpbird	$⊢ F \in B \to A \in (K^{ℕ_{0}})$
14	1 2 3 4	coe1sfi	$⊢ F \in B \to {finSupp}_{\underset{˙}{0}} (A)$
15	6 13 14	elrabd	$⊢ F \in B \to A \in \{g \in (K^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (g)\}$