This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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