# Metamath Proof Explorer

## Theorem lssvscl

Description: Closure of scalar product in a subspace. (Contributed by NM, 11-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lssvscl.f
`|- F = ( Scalar ` W )`
lssvscl.t
`|- .x. = ( .s ` W )`
lssvscl.b
`|- B = ( Base ` F )`
lssvscl.s
`|- S = ( LSubSp ` W )`
Assertion lssvscl
`|- ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> ( X .x. Y ) e. U )`

### Proof

Step Hyp Ref Expression
1 lssvscl.f
` |-  F = ( Scalar ` W )`
2 lssvscl.t
` |-  .x. = ( .s ` W )`
3 lssvscl.b
` |-  B = ( Base ` F )`
4 lssvscl.s
` |-  S = ( LSubSp ` W )`
5 simpll
` |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> W e. LMod )`
6 simprl
` |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> X e. B )`
7 eqid
` |-  ( Base ` W ) = ( Base ` W )`
8 7 4 lssel
` |-  ( ( U e. S /\ Y e. U ) -> Y e. ( Base ` W ) )`
` |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> Y e. ( Base ` W ) )`
10 7 1 2 3 lmodvscl
` |-  ( ( W e. LMod /\ X e. B /\ Y e. ( Base ` W ) ) -> ( X .x. Y ) e. ( Base ` W ) )`
11 5 6 9 10 syl3anc
` |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> ( X .x. Y ) e. ( Base ` W ) )`
12 eqid
` |-  ( +g ` W ) = ( +g ` W )`
13 eqid
` |-  ( 0g ` W ) = ( 0g ` W )`
14 7 12 13 lmod0vrid
` |-  ( ( W e. LMod /\ ( X .x. Y ) e. ( Base ` W ) ) -> ( ( X .x. Y ) ( +g ` W ) ( 0g ` W ) ) = ( X .x. Y ) )`
15 5 11 14 syl2anc
` |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> ( ( X .x. Y ) ( +g ` W ) ( 0g ` W ) ) = ( X .x. Y ) )`
16 simplr
` |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> U e. S )`
17 simprr
` |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> Y e. U )`
18 13 4 lss0cl
` |-  ( ( W e. LMod /\ U e. S ) -> ( 0g ` W ) e. U )`
` |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> ( 0g ` W ) e. U )`
` |-  ( ( U e. S /\ ( X e. B /\ Y e. U /\ ( 0g ` W ) e. U ) ) -> ( ( X .x. Y ) ( +g ` W ) ( 0g ` W ) ) e. U )`
` |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> ( ( X .x. Y ) ( +g ` W ) ( 0g ` W ) ) e. U )`
` |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> ( X .x. Y ) e. U )`