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 โŠข ๐‘‰ = ( Base โ€˜ ๐‘Š )
lssss.s โŠข ๐‘† = ( LSubSp โ€˜ ๐‘Š )
Assertion lss1 ( ๐‘Š โˆˆ LMod โ†’ ๐‘‰ โˆˆ ๐‘† )

Proof

Step Hyp Ref Expression
1 lssss.v โŠข ๐‘‰ = ( Base โ€˜ ๐‘Š )
2 lssss.s โŠข ๐‘† = ( LSubSp โ€˜ ๐‘Š )
3 eqidd โŠข ( ๐‘Š โˆˆ LMod โ†’ ( Scalar โ€˜ ๐‘Š ) = ( Scalar โ€˜ ๐‘Š ) )
4 eqidd โŠข ( ๐‘Š โˆˆ LMod โ†’ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) )
5 1 a1i โŠข ( ๐‘Š โˆˆ LMod โ†’ ๐‘‰ = ( Base โ€˜ ๐‘Š ) )
6 eqidd โŠข ( ๐‘Š โˆˆ LMod โ†’ ( +g โ€˜ ๐‘Š ) = ( +g โ€˜ ๐‘Š ) )
7 eqidd โŠข ( ๐‘Š โˆˆ LMod โ†’ ( ยท๐‘  โ€˜ ๐‘Š ) = ( ยท๐‘  โ€˜ ๐‘Š ) )
8 2 a1i โŠข ( ๐‘Š โˆˆ LMod โ†’ ๐‘† = ( LSubSp โ€˜ ๐‘Š ) )
9 ssidd โŠข ( ๐‘Š โˆˆ LMod โ†’ ๐‘‰ โŠ† ๐‘‰ )
10 1 lmodbn0 โŠข ( ๐‘Š โˆˆ LMod โ†’ ๐‘‰ โ‰  โˆ… )
11 simpl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰ ) ) โ†’ ๐‘Š โˆˆ LMod )
12 eqid โŠข ( Scalar โ€˜ ๐‘Š ) = ( Scalar โ€˜ ๐‘Š )
13 eqid โŠข ( ยท๐‘  โ€˜ ๐‘Š ) = ( ยท๐‘  โ€˜ ๐‘Š )
14 eqid โŠข ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) )
15 1 12 13 14 lmodvscl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘‰ ) โ†’ ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘Ž ) โˆˆ ๐‘‰ )
16 15 3adant3r3 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰ ) ) โ†’ ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘Ž ) โˆˆ ๐‘‰ )
17 simpr3 โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰ ) ) โ†’ ๐‘ โˆˆ ๐‘‰ )
18 eqid โŠข ( +g โ€˜ ๐‘Š ) = ( +g โ€˜ ๐‘Š )
19 1 18 lmodvacl โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘Ž ) โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰ ) โ†’ ( ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘Ž ) ( +g โ€˜ ๐‘Š ) ๐‘ ) โˆˆ ๐‘‰ )
20 11 16 17 19 syl3anc โŠข ( ( ๐‘Š โˆˆ LMod โˆง ( ๐‘ฅ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆง ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰ ) ) โ†’ ( ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘Ž ) ( +g โ€˜ ๐‘Š ) ๐‘ ) โˆˆ ๐‘‰ )
21 3 4 5 6 7 8 9 10 20 islssd โŠข ( ๐‘Š โˆˆ LMod โ†’ ๐‘‰ โˆˆ ๐‘† )