Theorem pserval2

Description: Value of the function G that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015)

	Ref	Expression
Hypothesis	pser.g	$$⊢G=\left(x\in ℂ⟼\left(n\in {\mathbb{N}}_0⟼A\left(n\right)x^n\right)\right)$$
Assertion	pserval2	$$⊢\left(X\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to G\left(X\right)\left(N\right)=A\left(N\right)X^N$$

Proof

Step	Hyp	Ref	Expression
1		pser.g	$$⊢G=\left(x\in ℂ⟼\left(n\in {\mathbb{N}}_0⟼A\left(n\right)x^n\right)\right)$$
2	1	pserval	$$⊢X\in ℂ\to G\left(X\right)=\left(y\in {\mathbb{N}}_0⟼A\left(y\right)X^y\right)$$
3	2	fveq1d	$$⊢X\in ℂ\to G\left(X\right)\left(N\right)=\left(y\in {\mathbb{N}}_0⟼A\left(y\right)X^y\right)\left(N\right)$$
4		fveq2	$$⊢y=N\to A\left(y\right)=A\left(N\right)$$
5		oveq2	$$⊢y=N\to X^y=X^N$$
6	4 5	oveq12d	$$⊢y=N\to A\left(y\right)X^y=A\left(N\right)X^N$$
7		eqid	$$⊢\left(y\in {\mathbb{N}}_0⟼A\left(y\right)X^y\right)=\left(y\in {\mathbb{N}}_0⟼A\left(y\right)X^y\right)$$
8		ovex	$$⊢A\left(N\right)X^N\in \mathrm{V}$$
9	6 7 8	fvmpt	$$⊢N\in {\mathbb{N}}_0\to \left(y\in {\mathbb{N}}_0⟼A\left(y\right)X^y\right)\left(N\right)=A\left(N\right)X^N$$
10	3 9	sylan9eq	$$⊢\left(X\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to G\left(X\right)\left(N\right)=A\left(N\right)X^N$$