Theorem coe1f2

Description: Functionality of univariate power series coefficient vectors. (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Hypotheses	coe1fval.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
	coe1f2.b	$$⊢B={\mathrm{Base}}_P$$
	coe1f2.p	$$⊢P={\mathrm{PwSer}}_1\left(R\right)$$
	coe1f2.k	$$⊢K={\mathrm{Base}}_R$$
Assertion	coe1f2	$$⊢F\in B\to A:{\mathbb{N}}_0⟶K$$

Proof

Step	Hyp	Ref	Expression
1		coe1fval.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
2		coe1f2.b	$$⊢B={\mathrm{Base}}_P$$
3		coe1f2.p	$$⊢P={\mathrm{PwSer}}_1\left(R\right)$$
4		coe1f2.k	$$⊢K={\mathrm{Base}}_R$$
5	3 2 4	psr1basf	$$⊢F\in B\to F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶K$$
6		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
7		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
8		0ex	$$⊢\varnothing \in \mathrm{V}$$
9		eqid	$$⊢\left(x\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{x\right\}\right)=\left(x\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{x\right\}\right)$$
10	6 7 8 9	mapsnf1o3	$$⊢\left(x\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{x\right\}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}{{\mathbb{N}}_0}^{1_{𝑜}}$$
11		f1of	$$⊢\left(x\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{x\right\}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}{{\mathbb{N}}_0}^{1_{𝑜}}\to \left(x\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{x\right\}\right):{\mathbb{N}}_0⟶{{\mathbb{N}}_0}^{1_{𝑜}}$$
12	10 11	ax-mp	$$⊢\left(x\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{x\right\}\right):{\mathbb{N}}_0⟶{{\mathbb{N}}_0}^{1_{𝑜}}$$
13		fco	$$⊢\left(F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶K\wedge \left(x\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{x\right\}\right):{\mathbb{N}}_0⟶{{\mathbb{N}}_0}^{1_{𝑜}}\right)\to \left(F\circ \left(x\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{x\right\}\right)\right):{\mathbb{N}}_0⟶K$$
14	5 12 13	sylancl	$$⊢F\in B\to \left(F\circ \left(x\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{x\right\}\right)\right):{\mathbb{N}}_0⟶K$$
15	1 2 3 9	coe1fval3	$$⊢F\in B\to A=F\circ \left(x\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{x\right\}\right)$$
16	15	feq1d	$$⊢F\in B\to \left(A:{\mathbb{N}}_0⟶K\leftrightarrow \left(F\circ \left(x\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{x\right\}\right)\right):{\mathbb{N}}_0⟶K\right)$$
17	14 16	mpbird	$$⊢F\in B\to A:{\mathbb{N}}_0⟶K$$