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

Metamath Proof Explorer

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 )