Description: Scalar multiplication for the dual of a vector space. (Contributed by NM, 19-Oct-2014) (Revised by Mario Carneiro, 22-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ldualsmul.f | |
|
ldualsmul.k | |
||
ldualsmul.t | |
||
ldualsmul.d | |
||
ldualsmul.r | |
||
ldualsmul.m | |
||
ldualsmul.w | |
||
ldualsmul.x | |
||
ldualsmul.y | |
||
Assertion | ldualsmul | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ldualsmul.f | |
|
2 | ldualsmul.k | |
|
3 | ldualsmul.t | |
|
4 | ldualsmul.d | |
|
5 | ldualsmul.r | |
|
6 | ldualsmul.m | |
|
7 | ldualsmul.w | |
|
8 | ldualsmul.x | |
|
9 | ldualsmul.y | |
|
10 | eqid | |
|
11 | 1 10 4 5 7 | ldualsca | |
12 | 11 | fveq2d | |
13 | 6 12 | eqtrid | |
14 | 13 | oveqd | |
15 | eqid | |
|
16 | 2 3 10 15 | opprmul | |
17 | 14 16 | eqtrdi | |