Theorem lspid

Description: The span of a subspace is itself. ( spanid analog.) (Contributed by NM, 15-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lspid.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lspid.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
Assertion	lspid	$$⊢\left(W\in \mathrm{LMod}\wedge U\in S\right)\to N\left(U\right)=U$$

Proof

Step	Hyp	Ref	Expression
1		lspid.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		lspid.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
4	3 1	lssss	$$⊢U\in S\to U\subseteq {\mathrm{Base}}_W$$
5	3 1 2	lspval	$$⊢\left(W\in \mathrm{LMod}\wedge U\subseteq {\mathrm{Base}}_W\right)\to N\left(U\right)=\bigcap \left\{t\in S|U\subseteq t\right\}$$
6	4 5	sylan2	$$⊢\left(W\in \mathrm{LMod}\wedge U\in S\right)\to N\left(U\right)=\bigcap \left\{t\in S|U\subseteq t\right\}$$
7		intmin	$$⊢U\in S\to \bigcap \left\{t\in S|U\subseteq t\right\}=U$$
8	7	adantl	$$⊢\left(W\in \mathrm{LMod}\wedge U\in S\right)\to \bigcap \left\{t\in S|U\subseteq t\right\}=U$$
9	6 8	eqtrd	$$⊢\left(W\in \mathrm{LMod}\wedge U\in S\right)\to N\left(U\right)=U$$