Theorem 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=\mathrm{Scalar}\left(W\right)$$
	ldualsmul.k	$$⊢K={\mathrm{Base}}_F$$
	ldualsmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_F$$
	ldualsmul.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualsmul.r	$$⊢R=\mathrm{Scalar}\left(D\right)$$
	ldualsmul.m	$$⊢\underset{\dot{}}{\bullet }={\cdot }_R$$
	ldualsmul.w	$$⊢\phi \to W\in V$$
	ldualsmul.x	$$⊢\phi \to X\in K$$
	ldualsmul.y	$$⊢\phi \to Y\in K$$
Assertion	ldualsmul	$$⊢\phi \to X\underset{\dot{}}{\bullet }Y=Y\underset{\dot{}}{·}X$$

Proof

Step	Hyp	Ref	Expression
1		ldualsmul.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		ldualsmul.k	$$⊢K={\mathrm{Base}}_F$$
3		ldualsmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_F$$
4		ldualsmul.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
5		ldualsmul.r	$$⊢R=\mathrm{Scalar}\left(D\right)$$
6		ldualsmul.m	$$⊢\underset{\dot{}}{\bullet }={\cdot }_R$$
7		ldualsmul.w	$$⊢\phi \to W\in V$$
8		ldualsmul.x	$$⊢\phi \to X\in K$$
9		ldualsmul.y	$$⊢\phi \to Y\in K$$
10		eqid	$$⊢{opp}_r\left(F\right)={opp}_r\left(F\right)$$
11	1 10 4 5 7	ldualsca	$$⊢\phi \to R={opp}_r\left(F\right)$$
12	11	fveq2d	$$⊢\phi \to {\cdot }_R={\cdot }_{{opp}_r\left(F\right)}$$
13	6 12	syl5eq	$$⊢\phi \to \underset{\dot{}}{\bullet }={\cdot }_{{opp}_r\left(F\right)}$$
14	13	oveqd	$$⊢\phi \to X\underset{\dot{}}{\bullet }Y=X{\cdot }_{{opp}_r\left(F\right)}Y$$
15		eqid	$$⊢{\cdot }_{{opp}_r\left(F\right)}={\cdot }_{{opp}_r\left(F\right)}$$
16	2 3 10 15	opprmul	$$⊢X{\cdot }_{{opp}_r\left(F\right)}Y=Y\underset{\dot{}}{·}X$$
17	14 16	eqtrdi	$$⊢\phi \to X\underset{\dot{}}{\bullet }Y=Y\underset{\dot{}}{·}X$$