Metamath Proof Explorer

Theorem lduallvec

Description: The dual of a left vector space is also a left vector space. Note that scalar multiplication is reversed by df-oppr ; otherwise, the dual would be a right vector space as is sometimes the case in the literature. (Contributed by NM, 22-Oct-2014)

Ref Expression
Hypotheses lduallvec.d ⊢ D = LDual ⁡ W
lduallvec.w ⊢ φ → W ∈ LVec
Assertion lduallvec ⊢ φ → D ∈ LVec

Proof

Step Hyp Ref Expression
1 lduallvec.d ⊢ D = LDual ⁡ W
2 lduallvec.w ⊢ φ → W ∈ LVec
3 lveclmod ⊢ W ∈ LVec → W ∈ LMod
4 2 3 syl ⊢ φ → W ∈ LMod
5 1 4 lduallmod ⊢ φ → D ∈ LMod
6 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
7 eqid ⊢ opp r ⁡ Scalar ⁡ W = opp r ⁡ Scalar ⁡ W
8 eqid ⊢ Scalar ⁡ D = Scalar ⁡ D
9 6 7 1 8 2 ldualsca ⊢ φ → Scalar ⁡ D = opp r ⁡ Scalar ⁡ W
10 6 lvecdrng ⊢ W ∈ LVec → Scalar ⁡ W ∈ DivRing
11 2 10 syl ⊢ φ → Scalar ⁡ W ∈ DivRing
12 7 opprdrng ⊢ Scalar ⁡ W ∈ DivRing ↔ opp r ⁡ Scalar ⁡ W ∈ DivRing
13 11 12 sylib ⊢ φ → opp r ⁡ Scalar ⁡ W ∈ DivRing
14 9 13 eqeltrd ⊢ φ → Scalar ⁡ D ∈ DivRing
15 8 islvec ⊢ D ∈ LVec ↔ D ∈ LMod ∧ Scalar ⁡ D ∈ DivRing
16 5 14 15 sylanbrc ⊢ φ → D ∈ LVec