Database
BASIC ALGEBRAIC STRUCTURES
Left modules
Subspaces and spans in a left module
lspsnss
Metamath Proof Explorer
Description: The span of the singleton of a subspace member is included in the
subspace. ( spansnss analog.) (Contributed by NM , 9-Apr-2014)
(Revised by Mario Carneiro , 4-Sep-2014)
Ref
Expression
Hypotheses
lspsnss.s
⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lspsnss.n
⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion
lspsnss
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
Proof
Step
Hyp
Ref
Expression
1
lspsnss.s
⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2
lspsnss.n
⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3
snssi
⊢ ( 𝑋 ∈ 𝑈 → { 𝑋 } ⊆ 𝑈 )
4
1 2
lspssp
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ { 𝑋 } ⊆ 𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
5
3 4
syl3an3
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )