# Metamath Proof Explorer

## Theorem lmodvscl

Description: Closure of scalar product for a left module. ( hvmulcl analog.) (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

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

### Proof

Step Hyp Ref Expression
1 lmodvscl.v
` |-  V = ( Base ` W )`
2 lmodvscl.f
` |-  F = ( Scalar ` W )`
3 lmodvscl.s
` |-  .x. = ( .s ` W )`
4 lmodvscl.k
` |-  K = ( Base ` F )`
5 biid
` |-  ( W e. LMod <-> W e. LMod )`
6 pm4.24
` |-  ( R e. K <-> ( R e. K /\ R e. K ) )`
7 pm4.24
` |-  ( X e. V <-> ( X e. V /\ X e. V ) )`
8 eqid
` |-  ( +g ` W ) = ( +g ` W )`
9 eqid
` |-  ( +g ` F ) = ( +g ` F )`
10 eqid
` |-  ( .r ` F ) = ( .r ` F )`
11 eqid
` |-  ( 1r ` F ) = ( 1r ` F )`
12 1 8 3 2 4 9 10 11 lmodlema
` |-  ( ( W e. LMod /\ ( R 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 ) ) /\ ( ( R ( +g ` F ) R ) .x. X ) = ( ( R .x. X ) ( +g ` W ) ( R .x. X ) ) ) /\ ( ( ( R ( .r ` F ) R ) .x. X ) = ( R .x. ( R .x. X ) ) /\ ( ( 1r ` F ) .x. X ) = X ) ) )`
13 12 simpld
` |-  ( ( W e. LMod /\ ( R 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 ) ) /\ ( ( R ( +g ` F ) R ) .x. X ) = ( ( R .x. X ) ( +g ` W ) ( R .x. X ) ) ) )`
14 13 simp1d
` |-  ( ( W e. LMod /\ ( R e. K /\ R e. K ) /\ ( X e. V /\ X e. V ) ) -> ( R .x. X ) e. V )`
15 5 6 7 14 syl3anb
` |-  ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( R .x. X ) e. V )`