ldualsmul

Description: Scalar multiplication for the dual of a vector space. (Contributed by NM, 19-Oct-2014) (Revised by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	ldualsmul.f	$⊢ F = Scalar (W)$
	ldualsmul.k	$⊢ K = {Base}_{F}$
	ldualsmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{F}$
	ldualsmul.d	$⊢ D = LDual (W)$
	ldualsmul.r	$⊢ R = Scalar (D)$
	ldualsmul.m	$⊢ \underset{˙}{∙} = \cdot_{R}$
	ldualsmul.w	$⊢ φ \to W \in V$
	ldualsmul.x	$⊢ φ \to X \in K$
	ldualsmul.y	$⊢ φ \to Y \in K$
Assertion	ldualsmul	$⊢ φ \to X \underset{˙}{∙} Y = Y \underset{˙}{\cdot} X$

Step	Hyp	Ref	Expression
1		ldualsmul.f	$⊢ F = Scalar (W)$
2		ldualsmul.k	$⊢ K = {Base}_{F}$
3		ldualsmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{F}$
4		ldualsmul.d	$⊢ D = LDual (W)$
5		ldualsmul.r	$⊢ R = Scalar (D)$
6		ldualsmul.m	$⊢ \underset{˙}{∙} = \cdot_{R}$
7		ldualsmul.w	$⊢ φ \to W \in V$
8		ldualsmul.x	$⊢ φ \to X \in K$
9		ldualsmul.y	$⊢ φ \to Y \in K$
10		eqid	$⊢ {opp}_{r} (F) = {opp}_{r} (F)$
11	1 10 4 5 7	ldualsca	$⊢ φ \to R = {opp}_{r} (F)$
12	11	fveq2d	$⊢ φ \to \cdot_{R} = \cdot_{{opp}_{r} (F)}$
13	6 12	eqtrid	$⊢ φ \to \underset{˙}{∙} = \cdot_{{opp}_{r} (F)}$
14	13	oveqd	$⊢ φ \to X \underset{˙}{∙} Y = X \cdot_{{opp}_{r} (F)} Y$
15		eqid	$⊢ \cdot_{{opp}_{r} (F)} = \cdot_{{opp}_{r} (F)}$
16	2 3 10 15	opprmul	$⊢ X \cdot_{{opp}_{r} (F)} Y = Y \underset{˙}{\cdot} X$
17	14 16	eqtrdi	$⊢ φ \to X \underset{˙}{∙} Y = Y \underset{˙}{\cdot} X$

Metamath Proof Explorer