Metamath Proof Explorer

Theorem lflvsass

Description: Associative law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014)

Ref Expression
Hypotheses lflass.v 
|- V = ( Base ` W )
lflass.r 
|- R = ( Scalar ` W )
lflass.k 
|- K = ( Base ` R )
lflass.t 
|- .x. = ( .r ` R )
lflass.f 
|- F = ( LFnl ` W )
lflass.w 
|- ( ph -> W e. LMod )
lflass.x 
|- ( ph -> X e. K )
lflass.y 
|- ( ph -> Y e. K )
lflass.g 
|- ( ph -> G e. F )
Assertion lflvsass 
|- ( ph -> ( G oF .x. ( V X. { ( X .x. Y ) } ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .x. ( V X. { Y } ) ) )

Proof

Step Hyp Ref Expression
1 lflass.v 
 |-  V = ( Base ` W )
2 lflass.r 
 |-  R = ( Scalar ` W )
3 lflass.k 
 |-  K = ( Base ` R )
4 lflass.t 
 |-  .x. = ( .r ` R )
5 lflass.f 
 |-  F = ( LFnl ` W )
6 lflass.w 
 |-  ( ph -> W e. LMod )
7 lflass.x 
 |-  ( ph -> X e. K )
8 lflass.y 
 |-  ( ph -> Y e. K )
9 lflass.g 
 |-  ( ph -> G e. F )
10 1 fvexi 
 |-  V e. _V
11 10 a1i 
 |-  ( ph -> V e. _V )
12 2 3 1 5 lflf 
 |-  ( ( W e. LMod /\ G e. F ) -> G : V --> K )
13 6 9 12 syl2anc 
 |-  ( ph -> G : V --> K )
14 fconst6g 
 |-  ( X e. K -> ( V X. { X } ) : V --> K )
15 7 14 syl 
 |-  ( ph -> ( V X. { X } ) : V --> K )
16 fconst6g 
 |-  ( Y e. K -> ( V X. { Y } ) : V --> K )
17 8 16 syl 
 |-  ( ph -> ( V X. { Y } ) : V --> K )
18 2 lmodring 
 |-  ( W e. LMod -> R e. Ring )
19 6 18 syl 
 |-  ( ph -> R e. Ring )
20 3 4 ringass 
 |-  ( ( R e. Ring /\ ( x e. K /\ y e. K /\ z e. K ) ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
21 19 20 sylan 
 |-  ( ( ph /\ ( x e. K /\ y e. K /\ z e. K ) ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
22 11 13 15 17 21 caofass 
 |-  ( ph -> ( ( G oF .x. ( V X. { X } ) ) oF .x. ( V X. { Y } ) ) = ( G oF .x. ( ( V X. { X } ) oF .x. ( V X. { Y } ) ) ) )
23 11 7 8 ofc12 
 |-  ( ph -> ( ( V X. { X } ) oF .x. ( V X. { Y } ) ) = ( V X. { ( X .x. Y ) } ) )
24 23 oveq2d 
 |-  ( ph -> ( G oF .x. ( ( V X. { X } ) oF .x. ( V X. { Y } ) ) ) = ( G oF .x. ( V X. { ( X .x. Y ) } ) ) )
25 22 24 eqtr2d 
 |-  ( ph -> ( G oF .x. ( V X. { ( X .x. Y ) } ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .x. ( V X. { Y } ) ) )