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 = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
Assertion	pserval	|- ( X e. CC -> ( G ` X ) = ( m e. NN0 |-> ( ( A ` m ) x. ( X ^ m ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pser.g	|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
2		oveq1	|- ( y = X -> ( y ^ m ) = ( X ^ m ) )
3	2	oveq2d	|- ( y = X -> ( ( A ` m ) x. ( y ^ m ) ) = ( ( A ` m ) x. ( X ^ m ) ) )
4	3	mpteq2dv	|- ( y = X -> ( m e. NN0 |-> ( ( A ` m ) x. ( y ^ m ) ) ) = ( m e. NN0 |-> ( ( A ` m ) x. ( X ^ m ) ) ) )
5		fveq2	|- ( n = m -> ( A ` n ) = ( A ` m ) )
6		oveq2	|- ( n = m -> ( x ^ n ) = ( x ^ m ) )
7	5 6	oveq12d	|- ( n = m -> ( ( A ` n ) x. ( x ^ n ) ) = ( ( A ` m ) x. ( x ^ m ) ) )
8	7	cbvmptv	|- ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) = ( m e. NN0 |-> ( ( A ` m ) x. ( x ^ m ) ) )
9		oveq1	|- ( x = y -> ( x ^ m ) = ( y ^ m ) )
10	9	oveq2d	|- ( x = y -> ( ( A ` m ) x. ( x ^ m ) ) = ( ( A ` m ) x. ( y ^ m ) ) )
11	10	mpteq2dv	|- ( x = y -> ( m e. NN0 |-> ( ( A ` m ) x. ( x ^ m ) ) ) = ( m e. NN0 |-> ( ( A ` m ) x. ( y ^ m ) ) ) )
12	8 11	syl5eq	|- ( x = y -> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) = ( m e. NN0 |-> ( ( A ` m ) x. ( y ^ m ) ) ) )
13	12	cbvmptv	|- ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) ) = ( y e. CC |-> ( m e. NN0 |-> ( ( A ` m ) x. ( y ^ m ) ) ) )
14	1 13	eqtri	|- G = ( y e. CC |-> ( m e. NN0 |-> ( ( A ` m ) x. ( y ^ m ) ) ) )
15		nn0ex	|- NN0 e. _V
16	15	mptex	|- ( m e. NN0 |-> ( ( A ` m ) x. ( X ^ m ) ) ) e. _V
17	4 14 16	fvmpt	|- ( X e. CC -> ( G ` X ) = ( m e. NN0 |-> ( ( A ` m ) x. ( X ^ m ) ) ) )