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 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )