Theorem mvrf2

Description: The power series/polynomial variable function maps indices to polynomials. (Contributed by Stefan O'Rear, 8-Mar-2015)

	Ref	Expression
Hypotheses	mvrf2.p	|- P = ( I mPoly R )
	mvrf2.v	|- V = ( I mVar R )
	mvrf2.b	|- B = ( Base ` P )
	mvrf2.i	|- ( ph -> I e. W )
	mvrf2.r	|- ( ph -> R e. Ring )
Assertion	mvrf2	|- ( ph -> V : I --> B )

Proof

Step	Hyp	Ref	Expression
1		mvrf2.p	|- P = ( I mPoly R )
2		mvrf2.v	|- V = ( I mVar R )
3		mvrf2.b	|- B = ( Base ` P )
4		mvrf2.i	|- ( ph -> I e. W )
5		mvrf2.r	|- ( ph -> R e. Ring )
6		eqid	|- ( I mPwSer R ) = ( I mPwSer R )
7		eqid	|- ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
8	6 2 7 4 5	mvrf	|- ( ph -> V : I --> ( Base ` ( I mPwSer R ) ) )
9	8	ffnd	|- ( ph -> V Fn I )
10	4	adantr	|- ( ( ph /\ x e. I ) -> I e. W )
11	5	adantr	|- ( ( ph /\ x e. I ) -> R e. Ring )
12		simpr	|- ( ( ph /\ x e. I ) -> x e. I )
13	1 2 3 10 11 12	mvrcl	|- ( ( ph /\ x e. I ) -> ( V ` x ) e. B )
14	13	ralrimiva	|- ( ph -> A. x e. I ( V ` x ) e. B )
15		ffnfv	|- ( V : I --> B <-> ( V Fn I /\ A. x e. I ( V ` x ) e. B ) )
16	9 14 15	sylanbrc	|- ( ph -> V : I --> B )