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 ) )
9 8 ad2ant2l 
 |-  ( ( ( 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 )
19 18 adantr 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> ( 0g ` W ) e. U )
20 1 3 12 2 4 lsscl 
 |-  ( ( U e. S /\ ( X e. B /\ Y e. U /\ ( 0g ` W ) e. U ) ) -> ( ( X .x. Y ) ( +g ` W ) ( 0g ` W ) ) e. U )
21 16 6 17 19 20 syl13anc 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> ( ( X .x. Y ) ( +g ` W ) ( 0g ` W ) ) e. U )
22 15 21 eqeltrrd 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. B /\ Y e. U ) ) -> ( X .x. Y ) e. U )