Metamath Proof Explorer


Theorem lduallmod

Description: The dual of a left module is also a left module. (Contributed by NM, 22-Oct-2014)

Ref Expression
Hypotheses lduallmod.d D = LDual W
lduallmod.w φ W LMod
Assertion lduallmod φ D LMod

Proof

Step Hyp Ref Expression
1 lduallmod.d D = LDual W
2 lduallmod.w φ W LMod
3 eqid Base W = Base W
4 eqid f + W = f + W
5 eqid LFnl W = LFnl W
6 eqid Scalar W = Scalar W
7 eqid Base Scalar W = Base Scalar W
8 eqid Scalar W = Scalar W
9 eqid opp r Scalar W = opp r Scalar W
10 eqid D = D
11 1 2 3 4 5 6 7 8 9 10 lduallmodlem φ D LMod