Theorem lcdsmul

Description: Scalar multiplication for the closed kernel vector space dual. (Contributed by NM, 20-Mar-2015)

	Ref	Expression
Hypotheses	lcdsmul.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdsmul.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdsmul.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
	lcdsmul.l	$$⊢L={\mathrm{Base}}_F$$
	lcdsmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_F$$
	lcdsmul.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdsmul.s	$$⊢S=\mathrm{Scalar}\left(C\right)$$
	lcdsmul.m	$$⊢\underset{\dot{}}{\bullet }={\cdot }_S$$
	lcdsmul.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcdsmul.x	$$⊢\phi \to X\in L$$
	lcdsmul.y	$$⊢\phi \to Y\in L$$
Assertion	lcdsmul	$$⊢\phi \to X\underset{\dot{}}{\bullet }Y=Y\underset{\dot{}}{·}X$$

Proof

Step	Hyp	Ref	Expression
1		lcdsmul.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdsmul.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcdsmul.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
4		lcdsmul.l	$$⊢L={\mathrm{Base}}_F$$
5		lcdsmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_F$$
6		lcdsmul.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
7		lcdsmul.s	$$⊢S=\mathrm{Scalar}\left(C\right)$$
8		lcdsmul.m	$$⊢\underset{\dot{}}{\bullet }={\cdot }_S$$
9		lcdsmul.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		lcdsmul.x	$$⊢\phi \to X\in L$$
11		lcdsmul.y	$$⊢\phi \to Y\in L$$
12		eqid	$$⊢{opp}_r\left(F\right)={opp}_r\left(F\right)$$
13	1 2 3 12 6 7 9	lcdsca	$$⊢\phi \to S={opp}_r\left(F\right)$$
14	13	fveq2d	$$⊢\phi \to {\cdot }_S={\cdot }_{{opp}_r\left(F\right)}$$
15	8 14	syl5eq	$$⊢\phi \to \underset{\dot{}}{\bullet }={\cdot }_{{opp}_r\left(F\right)}$$
16	15	oveqd	$$⊢\phi \to X\underset{\dot{}}{\bullet }Y=X{\cdot }_{{opp}_r\left(F\right)}Y$$
17		eqid	$$⊢{\cdot }_{{opp}_r\left(F\right)}={\cdot }_{{opp}_r\left(F\right)}$$
18	4 5 12 17	opprmul	$$⊢X{\cdot }_{{opp}_r\left(F\right)}Y=Y\underset{\dot{}}{·}X$$
19	16 18	eqtrdi	$$⊢\phi \to X\underset{\dot{}}{\bullet }Y=Y\underset{\dot{}}{·}X$$