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	$⊢ φ \to W \in LVec$
Assertion	lduallvec	$⊢ φ \to D \in LVec$

Proof

Step	Hyp	Ref	Expression
1		lduallvec.d	$⊢ D = LDual (W)$
2		lduallvec.w	$⊢ φ \to W \in LVec$
3		lveclmod	$⊢ W \in LVec \to W \in LMod$
4	2 3	syl	$⊢ φ \to W \in LMod$
5	1 4	lduallmod	$⊢ φ \to D \in 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	$⊢ φ \to Scalar (D) = {opp}_{r} (Scalar (W))$
10	6	lvecdrng	$⊢ W \in LVec \to Scalar (W) \in DivRing$
11	2 10	syl	$⊢ φ \to Scalar (W) \in DivRing$
12	7	opprdrng	$⊢ Scalar (W) \in DivRing \leftrightarrow {opp}_{r} (Scalar (W)) \in DivRing$
13	11 12	sylib	$⊢ φ \to {opp}_{r} (Scalar (W)) \in DivRing$
14	9 13	eqeltrd	$⊢ φ \to Scalar (D) \in DivRing$
15	8	islvec	$⊢ D \in LVec \leftrightarrow (D \in LMod \land Scalar (D) \in DivRing)$
16	5 14 15	sylanbrc	$⊢ φ \to D \in LVec$

Metamath Proof Explorer

Theorem lduallvec

Proof