Theorem pserval

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	pserval	$$⊢X\in ℂ\to G\left(X\right)=\left(m\in {\mathbb{N}}_0⟼A\left(m\right)X^m\right)$$

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		oveq1	$$⊢y=X\to y^m=X^m$$
3	2	oveq2d	$$⊢y=X\to A\left(m\right)y^m=A\left(m\right)X^m$$
4	3	mpteq2dv	$$⊢y=X\to \left(m\in {\mathbb{N}}_0⟼A\left(m\right)y^m\right)=\left(m\in {\mathbb{N}}_0⟼A\left(m\right)X^m\right)$$
5		fveq2	$$⊢n=m\to A\left(n\right)=A\left(m\right)$$
6		oveq2	$$⊢n=m\to x^n=x^m$$
7	5 6	oveq12d	$$⊢n=m\to A\left(n\right)x^n=A\left(m\right)x^m$$
8	7	cbvmptv	$$⊢\left(n\in {\mathbb{N}}_0⟼A\left(n\right)x^n\right)=\left(m\in {\mathbb{N}}_0⟼A\left(m\right)x^m\right)$$
9		oveq1	$$⊢x=y\to x^m=y^m$$
10	9	oveq2d	$$⊢x=y\to A\left(m\right)x^m=A\left(m\right)y^m$$
11	10	mpteq2dv	$$⊢x=y\to \left(m\in {\mathbb{N}}_0⟼A\left(m\right)x^m\right)=\left(m\in {\mathbb{N}}_0⟼A\left(m\right)y^m\right)$$
12	8 11	eqtrid	$$⊢x=y\to \left(n\in {\mathbb{N}}_0⟼A\left(n\right)x^n\right)=\left(m\in {\mathbb{N}}_0⟼A\left(m\right)y^m\right)$$
13	12	cbvmptv	$$⊢\left(x\in ℂ⟼\left(n\in {\mathbb{N}}_0⟼A\left(n\right)x^n\right)\right)=\left(y\in ℂ⟼\left(m\in {\mathbb{N}}_0⟼A\left(m\right)y^m\right)\right)$$
14	1 13	eqtri	$$⊢G=\left(y\in ℂ⟼\left(m\in {\mathbb{N}}_0⟼A\left(m\right)y^m\right)\right)$$
15		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
16	15	mptex	$$⊢\left(m\in {\mathbb{N}}_0⟼A\left(m\right)X^m\right)\in \mathrm{V}$$
17	4 14 16	fvmpt	$$⊢X\in ℂ\to G\left(X\right)=\left(m\in {\mathbb{N}}_0⟼A\left(m\right)X^m\right)$$