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 )