Theorem elspansn3

Description: A member of the span of the singleton of a vector is a member of a subspace containing the vector. (Contributed by NM, 16-Dec-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	elspansn3	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ ( span ‘ { 𝐵 } ) ) → 𝐶 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		spansnss	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ) → ( span ‘ { 𝐵 } ) ⊆ 𝐴 )
2	1	sseld	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ) → ( 𝐶 ∈ ( span ‘ { 𝐵 } ) → 𝐶 ∈ 𝐴 ) )
3	2	3impia	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ ( span ‘ { 𝐵 } ) ) → 𝐶 ∈ 𝐴 )