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

Metamath Proof Explorer

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