This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( 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 ) )