Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Opposite rings and dual vector spaces
lduallmod
Next ⟩
lduallvec
Metamath Proof Explorer
Ascii
Unicode
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