Metamath Proof Explorer

Theorem lcdvsass

Description: Associative law for scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 lcdvsass.h 
 |-  H = ( LHyp ` K )
2 lcdvsass.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 lcdvsass.r 
 |-  R = ( Scalar ` U )
4 lcdvsass.l 
 |-  L = ( Base ` R )
5 lcdvsass.t 
 |-  .x. = ( .r ` R )
6 lcdvsass.d 
 |-  C = ( ( LCDual ` K ) ` W )
7 lcdvsass.f 
 |-  F = ( Base ` C )
8 lcdvsass.s 
 |-  .xb = ( .s ` C )
9 lcdvsass.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 lcdvsass.x 
 |-  ( ph -> X e. L )
11 lcdvsass.y 
 |-  ( ph -> Y e. L )
12 lcdvsass.g 
 |-  ( ph -> G e. F )
13 eqid 
 |-  ( Scalar ` C ) = ( Scalar ` C )
14 eqid 
 |-  ( .r ` ( Scalar ` C ) ) = ( .r ` ( Scalar ` C ) )
15 1 2 3 4 5 6 13 14 9 10 11 lcdsmul 
 |-  ( ph -> ( X ( .r ` ( Scalar ` C ) ) Y ) = ( Y .x. X ) )
16 15 oveq1d 
 |-  ( ph -> ( ( X ( .r ` ( Scalar ` C ) ) Y ) .xb G ) = ( ( Y .x. X ) .xb G ) )
17 1 6 9 lcdlmod 
 |-  ( ph -> C e. LMod )
18 eqid 
 |-  ( Base ` ( Scalar ` C ) ) = ( Base ` ( Scalar ` C ) )
19 1 2 3 4 6 13 18 9 lcdsbase 
 |-  ( ph -> ( Base ` ( Scalar ` C ) ) = L )
20 10 19 eleqtrrd 
 |-  ( ph -> X e. ( Base ` ( Scalar ` C ) ) )
21 11 19 eleqtrrd 
 |-  ( ph -> Y e. ( Base ` ( Scalar ` C ) ) )
22 7 13 8 18 14 lmodvsass 
 |-  ( ( C e. LMod /\ ( X e. ( Base ` ( Scalar ` C ) ) /\ Y e. ( Base ` ( Scalar ` C ) ) /\ G e. F ) ) -> ( ( X ( .r ` ( Scalar ` C ) ) Y ) .xb G ) = ( X .xb ( Y .xb G ) ) )
23 17 20 21 12 22 syl13anc 
 |-  ( ph -> ( ( X ( .r ` ( Scalar ` C ) ) Y ) .xb G ) = ( X .xb ( Y .xb G ) ) )
24 16 23 eqtr3d 
 |-  ( ph -> ( ( Y .x. X ) .xb G ) = ( X .xb ( Y .xb G ) ) )