Metamath Proof Explorer

Theorem lss1

Description: The set of vectors in a left module is a subspace. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lssss.v 
|- V = ( Base ` W )
lssss.s 
|- S = ( LSubSp ` W )
Assertion lss1 
|- ( W e. LMod -> V e. S )

Proof

Step Hyp Ref Expression
1 lssss.v 
 |-  V = ( Base ` W )
2 lssss.s 
 |-  S = ( LSubSp ` W )
3 eqidd 
 |-  ( W e. LMod -> ( Scalar ` W ) = ( Scalar ` W ) )
4 eqidd 
 |-  ( W e. LMod -> ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) )
5 1 a1i 
 |-  ( W e. LMod -> V = ( Base ` W ) )
6 eqidd 
 |-  ( W e. LMod -> ( +g ` W ) = ( +g ` W ) )
7 eqidd 
 |-  ( W e. LMod -> ( .s ` W ) = ( .s ` W ) )
8 2 a1i 
 |-  ( W e. LMod -> S = ( LSubSp ` W ) )
9 ssidd 
 |-  ( W e. LMod -> V C_ V )
10 1 lmodbn0 
 |-  ( W e. LMod -> V =/= (/) )
11 simpl 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. V /\ b e. V ) ) -> W e. LMod )
12 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
13 eqid 
 |-  ( .s ` W ) = ( .s ` W )
14 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
15 1 12 13 14 lmodvscl 
 |-  ( ( W e. LMod /\ x e. ( Base ` ( Scalar ` W ) ) /\ a e. V ) -> ( x ( .s ` W ) a ) e. V )
16 15 3adant3r3 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. V /\ b e. V ) ) -> ( x ( .s ` W ) a ) e. V )
17 simpr3 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. V /\ b e. V ) ) -> b e. V )
18 eqid 
 |-  ( +g ` W ) = ( +g ` W )
19 1 18 lmodvacl 
 |-  ( ( W e. LMod /\ ( x ( .s ` W ) a ) e. V /\ b e. V ) -> ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. V )
20 11 16 17 19 syl3anc 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. V /\ b e. V ) ) -> ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. V )
21 3 4 5 6 7 8 9 10 20 islssd 
 |-  ( W e. LMod -> V e. S )