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

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 ⊢ 𝐷 = ( LDual ‘ 𝑊 )
lduallvec.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
Assertion lduallvec ( 𝜑 → 𝐷 ∈ LVec )

Proof

Step Hyp Ref Expression
1 lduallvec.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
2 lduallvec.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
3 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
4 2 3 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 1 4 lduallmod ⊢ ( 𝜑 → 𝐷 ∈ LMod )
6 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
7 eqid ⊢ ( oppr ‘ ( Scalar ‘ 𝑊 ) ) = ( oppr ‘ ( Scalar ‘ 𝑊 ) )
8 eqid ⊢ ( Scalar ‘ 𝐷 ) = ( Scalar ‘ 𝐷 )
9 6 7 1 8 2 ldualsca ⊢ ( 𝜑 → ( Scalar ‘ 𝐷 ) = ( oppr ‘ ( Scalar ‘ 𝑊 ) ) )
10 6 lvecdrng ⊢ ( 𝑊 ∈ LVec → ( Scalar ‘ 𝑊 ) ∈ DivRing )
11 2 10 syl ⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ DivRing )
12 7 opprdrng ⊢ ( ( Scalar ‘ 𝑊 ) ∈ DivRing ↔ ( oppr ‘ ( Scalar ‘ 𝑊 ) ) ∈ DivRing )
13 11 12 sylib ⊢ ( 𝜑 → ( oppr ‘ ( Scalar ‘ 𝑊 ) ) ∈ DivRing )
14 9 13 eqeltrd ⊢ ( 𝜑 → ( Scalar ‘ 𝐷 ) ∈ DivRing )
15 8 islvec ⊢ ( 𝐷 ∈ LVec ↔ ( 𝐷 ∈ LMod ∧ ( Scalar ‘ 𝐷 ) ∈ DivRing ) )
16 5 14 15 sylanbrc ⊢ ( 𝜑 → 𝐷 ∈ LVec )