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 → 𝑉 ∈ 𝑆 )