Metamath Proof Explorer


Theorem lspsnid

Description: A vector belongs to the span of its singleton. ( spansnid analog.) (Contributed by NM, 9-Apr-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lspsnid.v 𝑉 = ( Base ‘ 𝑊 )
lspsnid.n 𝑁 = ( LSpan ‘ 𝑊 )
Assertion lspsnid ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 lspsnid.v 𝑉 = ( Base ‘ 𝑊 )
2 lspsnid.n 𝑁 = ( LSpan ‘ 𝑊 )
3 snssi ( 𝑋𝑉 → { 𝑋 } ⊆ 𝑉 )
4 1 2 lspssid ( ( 𝑊 ∈ LMod ∧ { 𝑋 } ⊆ 𝑉 ) → { 𝑋 } ⊆ ( 𝑁 ‘ { 𝑋 } ) )
5 3 4 sylan2 ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → { 𝑋 } ⊆ ( 𝑁 ‘ { 𝑋 } ) )
6 snssg ( 𝑋𝑉 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ { 𝑋 } ⊆ ( 𝑁 ‘ { 𝑋 } ) ) )
7 6 adantl ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ { 𝑋 } ⊆ ( 𝑁 ‘ { 𝑋 } ) ) )
8 5 7 mpbird ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )