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 )