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 ∈ LMod → V ∈ S

Proof

Step Hyp Ref Expression
1 lssss.v ⊢ V = Base W
2 lssss.s ⊢ S = LSubSp ⁡ W
3 eqidd ⊢ W ∈ LMod → Scalar ⁡ W = Scalar ⁡ W
4 eqidd ⊢ W ∈ LMod → Base Scalar ⁡ W = Base Scalar ⁡ W
5 1 a1i ⊢ W ∈ LMod → V = Base W
6 eqidd ⊢ W ∈ LMod → + W = + W
7 eqidd ⊢ W ∈ LMod → ⋅ W = ⋅ W
8 2 a1i ⊢ W ∈ LMod → S = LSubSp ⁡ W
9 ssidd ⊢ W ∈ LMod → V ⊆ V
10 1 lmodbn0 ⊢ W ∈ LMod → V ≠ ∅
11 simpl ⊢ W ∈ LMod ∧ x ∈ Base Scalar ⁡ W ∧ a ∈ V ∧ b ∈ V → W ∈ LMod
12 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
13 eqid ⊢ ⋅ W = ⋅ W
14 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
15 1 12 13 14 lmodvscl ⊢ W ∈ LMod ∧ x ∈ Base Scalar ⁡ W ∧ a ∈ V → x ⋅ W a ∈ V
16 15 3adant3r3 ⊢ W ∈ LMod ∧ x ∈ Base Scalar ⁡ W ∧ a ∈ V ∧ b ∈ V → x ⋅ W a ∈ V
17 simpr3 ⊢ W ∈ LMod ∧ x ∈ Base Scalar ⁡ W ∧ a ∈ V ∧ b ∈ V → b ∈ V
18 eqid ⊢ + W = + W
19 1 18 lmodvacl ⊢ W ∈ LMod ∧ x ⋅ W a ∈ V ∧ b ∈ V → x ⋅ W a + W b ∈ V
20 11 16 17 19 syl3anc ⊢ W ∈ LMod ∧ x ∈ Base Scalar ⁡ W ∧ a ∈ V ∧ b ∈ V → x ⋅ W a + W b ∈ V
21 3 4 5 6 7 8 9 10 20 islssd ⊢ W ∈ LMod → V ∈ S