Theorem spansnss2

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

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

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	ex	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to \left(B\in A\to \mathrm{span}\left(\left\{B\right\}\right)\subseteq A\right)$$
3	2	adantr	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in \mathscr{H}\right)\to \left(B\in A\to \mathrm{span}\left(\left\{B\right\}\right)\subseteq A\right)$$
4		spansnid	$$⊢B\in \mathscr{H}\to B\in \mathrm{span}\left(\left\{B\right\}\right)$$
5		ssel	$$⊢\mathrm{span}\left(\left\{B\right\}\right)\subseteq A\to \left(B\in \mathrm{span}\left(\left\{B\right\}\right)\to B\in A\right)$$
6	4 5	syl5com	$$⊢B\in \mathscr{H}\to \left(\mathrm{span}\left(\left\{B\right\}\right)\subseteq A\to B\in A\right)$$
7	6	adantl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in \mathscr{H}\right)\to \left(\mathrm{span}\left(\left\{B\right\}\right)\subseteq A\to B\in A\right)$$
8	3 7	impbid	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in \mathscr{H}\right)\to \left(B\in A\leftrightarrow \mathrm{span}\left(\left\{B\right\}\right)\subseteq A\right)$$