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

Metamath Proof Explorer

Theorem psrelbas

Description: An element of the set of power series is a function on the coefficients. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses psrbas.s 
|- S = ( I mPwSer R )
psrbas.k 
|- K = ( Base ` R )
psrbas.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
psrbas.b 
|- B = ( Base ` S )
psrelbas.x 
|- ( ph -> X e. B )
Assertion psrelbas 
|- ( ph -> X : D --> K )

Proof

Step Hyp Ref Expression
1 psrbas.s 
 |-  S = ( I mPwSer R )
2 psrbas.k 
 |-  K = ( Base ` R )
3 psrbas.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
4 psrbas.b 
 |-  B = ( Base ` S )
5 psrelbas.x 
 |-  ( ph -> X e. B )
6 reldmpsr 
 |-  Rel dom mPwSer
7 6 1 4 elbasov 
 |-  ( X e. B -> ( I e. _V /\ R e. _V ) )
8 5 7 syl 
 |-  ( ph -> ( I e. _V /\ R e. _V ) )
9 8 simpld 
 |-  ( ph -> I e. _V )
10 1 2 3 4 9 psrbas 
 |-  ( ph -> B = ( K ^m D ) )
11 5 10 eleqtrd 
 |-  ( ph -> X e. ( K ^m D ) )
12 2 fvexi 
 |-  K e. _V
13 ovex 
 |-  ( NN0 ^m I ) e. _V
14 3 13 rabex2 
 |-  D e. _V
15 12 14 elmap 
 |-  ( X e. ( K ^m D ) <-> X : D --> K )
16 11 15 sylib 
 |-  ( ph -> X : D --> K )