Theorem elspancl

Description: A member of a span is a vector. (Contributed by NM, 17-Dec-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	elspancl	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ∈ ( span ‘ 𝐴 ) ) → 𝐵 ∈ ℋ )

Proof

Step	Hyp	Ref	Expression
1		spancl	⊢ ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) ∈ Sℋ )
2		shel	⊢ ( ( ( span ‘ 𝐴 ) ∈ Sℋ ∧ 𝐵 ∈ ( span ‘ 𝐴 ) ) → 𝐵 ∈ ℋ )
3	1 2	sylan	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ∈ ( span ‘ 𝐴 ) ) → 𝐵 ∈ ℋ )