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 = ( Scalar ` W )
	ldualsmul.k	|- K = ( Base ` F )
	ldualsmul.t	|- .x. = ( .r ` F )
	ldualsmul.d	|- D = ( LDual ` W )
	ldualsmul.r	|- R = ( Scalar ` D )
	ldualsmul.m	|- .xb = ( .r ` R )
	ldualsmul.w	|- ( ph -> W e. V )
	ldualsmul.x	|- ( ph -> X e. K )
	ldualsmul.y	|- ( ph -> Y e. K )
Assertion	ldualsmul	|- ( ph -> ( X .xb Y ) = ( Y .x. X ) )

Proof

Step	Hyp	Ref	Expression
1		ldualsmul.f	|- F = ( Scalar ` W )
2		ldualsmul.k	|- K = ( Base ` F )
3		ldualsmul.t	|- .x. = ( .r ` F )
4		ldualsmul.d	|- D = ( LDual ` W )
5		ldualsmul.r	|- R = ( Scalar ` D )
6		ldualsmul.m	|- .xb = ( .r ` R )
7		ldualsmul.w	|- ( ph -> W e. V )
8		ldualsmul.x	|- ( ph -> X e. K )
9		ldualsmul.y	|- ( ph -> Y e. K )
10		eqid	|- ( oppR ` F ) = ( oppR ` F )
11	1 10 4 5 7	ldualsca	|- ( ph -> R = ( oppR ` F ) )
12	11	fveq2d	|- ( ph -> ( .r ` R ) = ( .r ` ( oppR ` F ) ) )
13	6 12	syl5eq	|- ( ph -> .xb = ( .r ` ( oppR ` F ) ) )
14	13	oveqd	|- ( ph -> ( X .xb Y ) = ( X ( .r ` ( oppR ` F ) ) Y ) )
15		eqid	|- ( .r ` ( oppR ` F ) ) = ( .r ` ( oppR ` F ) )
16	2 3 10 15	opprmul	|- ( X ( .r ` ( oppR ` F ) ) Y ) = ( Y .x. X )
17	14 16	eqtrdi	|- ( ph -> ( X .xb Y ) = ( Y .x. X ) )