Theorem spansnss

Description: The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 5-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	spansnss	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\right)\to \mathrm{span}\left(\left\{B\right\}\right)\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		shel	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\right)\to B\in \mathscr{H}$$
2		elspansn	$$⊢B\in \mathscr{H}\to \left(x\in \mathrm{span}\left(\left\{B\right\}\right)\leftrightarrow \exists y\in ℂx=y{\cdot }_{ℎ}B\right)$$
3	1 2	syl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\right)\to \left(x\in \mathrm{span}\left(\left\{B\right\}\right)\leftrightarrow \exists y\in ℂx=y{\cdot }_{ℎ}B\right)$$
4		shmulcl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge y\in ℂ\wedge B\in A\right)\to y{\cdot }_{ℎ}B\in A$$
5		eleq1a	$$⊢y{\cdot }_{ℎ}B\in A\to \left(x=y{\cdot }_{ℎ}B\to x\in A\right)$$
6	4 5	syl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge y\in ℂ\wedge B\in A\right)\to \left(x=y{\cdot }_{ℎ}B\to x\in A\right)$$
7	6	3exp	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to \left(y\in ℂ\to \left(B\in A\to \left(x=y{\cdot }_{ℎ}B\to x\in A\right)\right)\right)$$
8	7	com23	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to \left(B\in A\to \left(y\in ℂ\to \left(x=y{\cdot }_{ℎ}B\to x\in A\right)\right)\right)$$
9	8	imp	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\right)\to \left(y\in ℂ\to \left(x=y{\cdot }_{ℎ}B\to x\in A\right)\right)$$
10	9	rexlimdv	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\right)\to \left(\exists y\in ℂx=y{\cdot }_{ℎ}B\to x\in A\right)$$
11	3 10	sylbid	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\right)\to \left(x\in \mathrm{span}\left(\left\{B\right\}\right)\to x\in A\right)$$
12	11	ssrdv	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in A\right)\to \mathrm{span}\left(\left\{B\right\}\right)\subseteq A$$