Theorem coe1fval3

Description: Univariate power series coefficient vectors expressed as a function composition. (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)$$
	coe1fval3.g	$$⊢G=\left(y\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{y\right\}\right)$$
Assertion	coe1fval3	$$⊢F\in B\to A=F\circ G$$

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		coe1fval3.g	$$⊢G=\left(y\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{y\right\}\right)$$
5	1	coe1fval	$$⊢F\in B\to A=\left(y\in {\mathbb{N}}_0⟼F\left(1_{𝑜}\times \left\{y\right\}\right)\right)$$
6		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
7	3 2 6	psr1basf	$$⊢F\in B\to F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶{\mathrm{Base}}_R$$
8		ssv	$$⊢{\mathrm{Base}}_R\subseteq \mathrm{V}$$
9		fss	$$⊢\left(F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶{\mathrm{Base}}_R\wedge {\mathrm{Base}}_R\subseteq \mathrm{V}\right)\to F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶\mathrm{V}$$
10	7 8 9	sylancl	$$⊢F\in B\to F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶\mathrm{V}$$
11		fconst6g	$$⊢y\in {\mathbb{N}}_0\to \left(1_{𝑜}\times \left\{y\right\}\right):1_{𝑜}⟶{\mathbb{N}}_0$$
12	11	adantl	$$⊢\left(F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶\mathrm{V}\wedge y\in {\mathbb{N}}_0\right)\to \left(1_{𝑜}\times \left\{y\right\}\right):1_{𝑜}⟶{\mathbb{N}}_0$$
13		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
14		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
15	13 14	elmap	$$⊢1_{𝑜}\times \left\{y\right\}\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\leftrightarrow \left(1_{𝑜}\times \left\{y\right\}\right):1_{𝑜}⟶{\mathbb{N}}_0$$
16	12 15	sylibr	$$⊢\left(F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶\mathrm{V}\wedge y\in {\mathbb{N}}_0\right)\to 1_{𝑜}\times \left\{y\right\}\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)$$
17	4	a1i	$$⊢F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶\mathrm{V}\to G=\left(y\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{y\right\}\right)$$
18		id	$$⊢F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶\mathrm{V}\to F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶\mathrm{V}$$
19	18	feqmptd	$$⊢F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶\mathrm{V}\to F=\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼F\left(x\right)\right)$$
20		fveq2	$$⊢x=1_{𝑜}\times \left\{y\right\}\to F\left(x\right)=F\left(1_{𝑜}\times \left\{y\right\}\right)$$
21	16 17 19 20	fmptco	$$⊢F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶\mathrm{V}\to F\circ G=\left(y\in {\mathbb{N}}_0⟼F\left(1_{𝑜}\times \left\{y\right\}\right)\right)$$
22	10 21	syl	$$⊢F\in B\to F\circ G=\left(y\in {\mathbb{N}}_0⟼F\left(1_{𝑜}\times \left\{y\right\}\right)\right)$$
23	5 22	eqtr4d	$$⊢F\in B\to A=F\circ G$$