Description: A power series variable is an element of the base set. (Contributed by Mario Carneiro, 29-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mvrf.s | |- S = ( I mPwSer R ) |
|
mvrf.v | |- V = ( I mVar R ) |
||
mvrf.b | |- B = ( Base ` S ) |
||
mvrf.i | |- ( ph -> I e. W ) |
||
mvrf.r | |- ( ph -> R e. Ring ) |
||
mvrcl2.x | |- ( ph -> X e. I ) |
||
Assertion | mvrcl2 | |- ( ph -> ( V ` X ) e. B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mvrf.s | |- S = ( I mPwSer R ) |
|
2 | mvrf.v | |- V = ( I mVar R ) |
|
3 | mvrf.b | |- B = ( Base ` S ) |
|
4 | mvrf.i | |- ( ph -> I e. W ) |
|
5 | mvrf.r | |- ( ph -> R e. Ring ) |
|
6 | mvrcl2.x | |- ( ph -> X e. I ) |
|
7 | 1 2 3 4 5 | mvrf | |- ( ph -> V : I --> B ) |
8 | 7 6 | ffvelrnd | |- ( ph -> ( V ` X ) e. B ) |