Metamath Proof Explorer

Theorem lssvacl

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

Ref Expression
Hypotheses lssvacl.p 
|- .+ = ( +g ` W )
lssvacl.s 
|- S = ( LSubSp ` W )
Assertion lssvacl 
|- ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( X .+ Y ) e. U )

Proof

Step Hyp Ref Expression
1 lssvacl.p 
 |-  .+ = ( +g ` W )
2 lssvacl.s 
 |-  S = ( LSubSp ` W )
3 simpll 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> W e. LMod )
4 eqid 
 |-  ( Base ` W ) = ( Base ` W )
5 4 2 lssel 
 |-  ( ( U e. S /\ X e. U ) -> X e. ( Base ` W ) )
6 5 ad2ant2lr 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> X e. ( Base ` W ) )
7 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
8 eqid 
 |-  ( .s ` W ) = ( .s ` W )
9 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
10 4 7 8 9 lmodvs1 
 |-  ( ( W e. LMod /\ X e. ( Base ` W ) ) -> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) X ) = X )
11 3 6 10 syl2anc 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) X ) = X )
12 11 oveq1d 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) X ) .+ Y ) = ( X .+ Y ) )
13 simplr 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> U e. S )
14 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
15 7 14 9 lmod1cl 
 |-  ( W e. LMod -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
16 15 ad2antrr 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
17 simprl 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> X e. U )
18 simprr 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> Y e. U )
19 7 14 1 8 2 lsscl 
 |-  ( ( U e. S /\ ( ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) /\ X e. U /\ Y e. U ) ) -> ( ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) X ) .+ Y ) e. U )
20 13 16 17 18 19 syl13anc 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) X ) .+ Y ) e. U )
21 12 20 eqeltrrd 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( X e. U /\ Y e. U ) ) -> ( X .+ Y ) e. U )