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 = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
Assertion	pserval2	|- ( ( X e. CC /\ N e. NN0 ) -> ( ( G ` X ) ` N ) = ( ( A ` N ) x. ( X ^ N ) ) )

Proof

Step	Hyp	Ref	Expression
1		pser.g	|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
2	1	pserval	|- ( X e. CC -> ( G ` X ) = ( y e. NN0 |-> ( ( A ` y ) x. ( X ^ y ) ) ) )
3	2	fveq1d	|- ( X e. CC -> ( ( G ` X ) ` N ) = ( ( y e. NN0 |-> ( ( A ` y ) x. ( X ^ y ) ) ) ` N ) )
4		fveq2	|- ( y = N -> ( A ` y ) = ( A ` N ) )
5		oveq2	|- ( y = N -> ( X ^ y ) = ( X ^ N ) )
6	4 5	oveq12d	|- ( y = N -> ( ( A ` y ) x. ( X ^ y ) ) = ( ( A ` N ) x. ( X ^ N ) ) )
7		eqid	|- ( y e. NN0 |-> ( ( A ` y ) x. ( X ^ y ) ) ) = ( y e. NN0 |-> ( ( A ` y ) x. ( X ^ y ) ) )
8		ovex	|- ( ( A ` N ) x. ( X ^ N ) ) e. _V
9	6 7 8	fvmpt	|- ( N e. NN0 -> ( ( y e. NN0 |-> ( ( A ` y ) x. ( X ^ y ) ) ) ` N ) = ( ( A ` N ) x. ( X ^ N ) ) )
10	3 9	sylan9eq	|- ( ( X e. CC /\ N e. NN0 ) -> ( ( G ` X ) ` N ) = ( ( A ` N ) x. ( X ^ N ) ) )