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