Description: Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mvrfval.v | |
|
mvrfval.d | |
||
mvrfval.z | |
||
mvrfval.o | |
||
mvrfval.i | |
||
mvrfval.r | |
||
mvrval.x | |
||
mvrval2.f | |
||
Assertion | mvrval2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mvrfval.v | |
|
2 | mvrfval.d | |
|
3 | mvrfval.z | |
|
4 | mvrfval.o | |
|
5 | mvrfval.i | |
|
6 | mvrfval.r | |
|
7 | mvrval.x | |
|
8 | mvrval2.f | |
|
9 | 1 2 3 4 5 6 7 | mvrval | |
10 | 9 | fveq1d | |
11 | eqeq1 | |
|
12 | 11 | ifbid | |
13 | eqid | |
|
14 | 4 | fvexi | |
15 | 3 | fvexi | |
16 | 14 15 | ifex | |
17 | 12 13 16 | fvmpt | |
18 | 8 17 | syl | |
19 | 10 18 | eqtrd | |