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 
|- D = ( LDual ` W )
lduallvec.w 
|- ( ph -> W e. LVec )
Assertion lduallvec 
|- ( ph -> D e. LVec )

Proof

Step Hyp Ref Expression
1 lduallvec.d 
 |-  D = ( LDual ` W )
2 lduallvec.w 
 |-  ( ph -> W e. LVec )
3 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
4 2 3 syl 
 |-  ( ph -> W e. LMod )
5 1 4 lduallmod 
 |-  ( ph -> D e. LMod )
6 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
7 eqid 
 |-  ( oppR ` ( Scalar ` W ) ) = ( oppR ` ( Scalar ` W ) )
8 eqid 
 |-  ( Scalar ` D ) = ( Scalar ` D )
9 6 7 1 8 2 ldualsca 
 |-  ( ph -> ( Scalar ` D ) = ( oppR ` ( Scalar ` W ) ) )
10 6 lvecdrng 
 |-  ( W e. LVec -> ( Scalar ` W ) e. DivRing )
11 2 10 syl 
 |-  ( ph -> ( Scalar ` W ) e. DivRing )
12 7 opprdrng 
 |-  ( ( Scalar ` W ) e. DivRing <-> ( oppR ` ( Scalar ` W ) ) e. DivRing )
13 11 12 sylib 
 |-  ( ph -> ( oppR ` ( Scalar ` W ) ) e. DivRing )
14 9 13 eqeltrd 
 |-  ( ph -> ( Scalar ` D ) e. DivRing )
15 8 islvec 
 |-  ( D e. LVec <-> ( D e. LMod /\ ( Scalar ` D ) e. DivRing ) )
16 5 14 15 sylanbrc 
 |-  ( ph -> D e. LVec )