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	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\wedge C\in \mathrm{span}\left(\left\{B\right\}\right)\right)\to C\in A$$

Proof

Step	Hyp	Ref	Expression
1		spansnss	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\right)\to \mathrm{span}\left(\left\{B\right\}\right)\subseteq A$$
2	1	sseld	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\right)\to \left(C\in \mathrm{span}\left(\left\{B\right\}\right)\to C\in A\right)$$
3	2	3impia	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\wedge C\in \mathrm{span}\left(\left\{B\right\}\right)\right)\to C\in A$$