Metamath Proof Explorer

Theorem lmodvsass

Description: Associative law for scalar product. ( ax-hvmulass analog.) (Contributed by NM, 10-Jan-2014) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses lmodvsass.v 
|- V = ( Base ` W )
lmodvsass.f 
|- F = ( Scalar ` W )
lmodvsass.s 
|- .x. = ( .s ` W )
lmodvsass.k 
|- K = ( Base ` F )
lmodvsass.t 
|- .X. = ( .r ` F )
Assertion lmodvsass 
|- ( ( W e. LMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q .X. R ) .x. X ) = ( Q .x. ( R .x. X ) ) )

Proof

Step Hyp Ref Expression
1 lmodvsass.v 
 |-  V = ( Base ` W )
2 lmodvsass.f 
 |-  F = ( Scalar ` W )
3 lmodvsass.s 
 |-  .x. = ( .s ` W )
4 lmodvsass.k 
 |-  K = ( Base ` F )
5 lmodvsass.t 
 |-  .X. = ( .r ` F )
6 eqid 
 |-  ( +g ` W ) = ( +g ` W )
7 eqid 
 |-  ( +g ` F ) = ( +g ` F )
8 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
9 1 6 3 2 4 7 5 8 lmodlema 
 |-  ( ( W e. LMod /\ ( Q e. K /\ R e. K ) /\ ( X e. V /\ X e. V ) ) -> ( ( ( R .x. X ) e. V /\ ( R .x. ( X ( +g ` W ) X ) ) = ( ( R .x. X ) ( +g ` W ) ( R .x. X ) ) /\ ( ( Q ( +g ` F ) R ) .x. X ) = ( ( Q .x. X ) ( +g ` W ) ( R .x. X ) ) ) /\ ( ( ( Q .X. R ) .x. X ) = ( Q .x. ( R .x. X ) ) /\ ( ( 1r ` F ) .x. X ) = X ) ) )
10 9 simprld 
 |-  ( ( W e. LMod /\ ( Q e. K /\ R e. K ) /\ ( X e. V /\ X e. V ) ) -> ( ( Q .X. R ) .x. X ) = ( Q .x. ( R .x. X ) ) )
11 10 3expa 
 |-  ( ( ( W e. LMod /\ ( Q e. K /\ R e. K ) ) /\ ( X e. V /\ X e. V ) ) -> ( ( Q .X. R ) .x. X ) = ( Q .x. ( R .x. X ) ) )
12 11 anabsan2 
 |-  ( ( ( W e. LMod /\ ( Q e. K /\ R e. K ) ) /\ X e. V ) -> ( ( Q .X. R ) .x. X ) = ( Q .x. ( R .x. X ) ) )
13 12 exp42 
 |-  ( W e. LMod -> ( Q e. K -> ( R e. K -> ( X e. V -> ( ( Q .X. R ) .x. X ) = ( Q .x. ( R .x. X ) ) ) ) ) )
14 13 3imp2 
 |-  ( ( W e. LMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q .X. R ) .x. X ) = ( Q .x. ( R .x. X ) ) )