# 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 ) ) )`