This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )