Theorem lcdsmul

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

	Ref	Expression
Hypotheses	lcdsmul.h	|- H = ( LHyp ` K )
	lcdsmul.u	|- U = ( ( DVecH ` K ) ` W )
	lcdsmul.f	|- F = ( Scalar ` U )
	lcdsmul.l	|- L = ( Base ` F )
	lcdsmul.t	|- .x. = ( .r ` F )
	lcdsmul.c	|- C = ( ( LCDual ` K ) ` W )
	lcdsmul.s	|- S = ( Scalar ` C )
	lcdsmul.m	|- .xb = ( .r ` S )
	lcdsmul.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lcdsmul.x	|- ( ph -> X e. L )
	lcdsmul.y	|- ( ph -> Y e. L )
Assertion	lcdsmul	|- ( ph -> ( X .xb Y ) = ( Y .x. X ) )

Proof

Step	Hyp	Ref	Expression
1		lcdsmul.h	|- H = ( LHyp ` K )
2		lcdsmul.u	|- U = ( ( DVecH ` K ) ` W )
3		lcdsmul.f	|- F = ( Scalar ` U )
4		lcdsmul.l	|- L = ( Base ` F )
5		lcdsmul.t	|- .x. = ( .r ` F )
6		lcdsmul.c	|- C = ( ( LCDual ` K ) ` W )
7		lcdsmul.s	|- S = ( Scalar ` C )
8		lcdsmul.m	|- .xb = ( .r ` S )
9		lcdsmul.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		lcdsmul.x	|- ( ph -> X e. L )
11		lcdsmul.y	|- ( ph -> Y e. L )
12		eqid	|- ( oppR ` F ) = ( oppR ` F )
13	1 2 3 12 6 7 9	lcdsca	|- ( ph -> S = ( oppR ` F ) )
14	13	fveq2d	|- ( ph -> ( .r ` S ) = ( .r ` ( oppR ` F ) ) )
15	8 14	syl5eq	|- ( ph -> .xb = ( .r ` ( oppR ` F ) ) )
16	15	oveqd	|- ( ph -> ( X .xb Y ) = ( X ( .r ` ( oppR ` F ) ) Y ) )
17		eqid	|- ( .r ` ( oppR ` F ) ) = ( .r ` ( oppR ` F ) )
18	4 5 12 17	opprmul	|- ( X ( .r ` ( oppR ` F ) ) Y ) = ( Y .x. X )
19	16 18	eqtrdi	|- ( ph -> ( X .xb Y ) = ( Y .x. X ) )