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 )