Metamath Proof Explorer


Theorem ldualsmul

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 F=ScalarW
ldualsmul.k K=BaseF
ldualsmul.t ·˙=F
ldualsmul.d D=LDualW
ldualsmul.r R=ScalarD
ldualsmul.m ˙=R
ldualsmul.w φWV
ldualsmul.x φXK
ldualsmul.y φYK
Assertion ldualsmul φX˙Y=Y·˙X

Proof

Step Hyp Ref Expression
1 ldualsmul.f F=ScalarW
2 ldualsmul.k K=BaseF
3 ldualsmul.t ·˙=F
4 ldualsmul.d D=LDualW
5 ldualsmul.r R=ScalarD
6 ldualsmul.m ˙=R
7 ldualsmul.w φWV
8 ldualsmul.x φXK
9 ldualsmul.y φYK
10 eqid opprF=opprF
11 1 10 4 5 7 ldualsca φR=opprF
12 11 fveq2d φR=opprF
13 6 12 eqtrid φ˙=opprF
14 13 oveqd φX˙Y=XopprFY
15 eqid opprF=opprF
16 2 3 10 15 opprmul XopprFY=Y·˙X
17 14 16 eqtrdi φX˙Y=Y·˙X