Database
BASIC ALGEBRAIC STRUCTURES
Left modules
Subspaces and spans in a left module
lspsnel3
Metamath Proof Explorer
Description: A member of the span of the singleton of a vector is a member of a
subspace containing the vector. ( elspansn3 analog.) (Contributed by NM , 4-Jul-2014)
Ref
Expression
Hypotheses
lspsnss.s
⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lspsnss.n
⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspsnel3.w
⊢ ( 𝜑 → 𝑊 ∈ LMod )
lspsnel3.u
⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lspsnel3.x
⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
lspsnel3.y
⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) )
Assertion
lspsnel3
⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
Proof
Step
Hyp
Ref
Expression
1
lspsnss.s
⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2
lspsnss.n
⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3
lspsnel3.w
⊢ ( 𝜑 → 𝑊 ∈ LMod )
4
lspsnel3.u
⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
5
lspsnel3.x
⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
6
lspsnel3.y
⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) )
7
1 2
lspsnss
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
8
3 4 5 7
syl3anc
⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
9
8 6
sseldd
⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )