Theorem lss0ss

Description: The zero subspace is included in every subspace. ( sh0le analog.) (Contributed by NM, 27-Mar-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lss0cl.z	$$⊢\underset{\dot{}}{0}=0_W$$
	lss0cl.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
Assertion	lss0ss	$$⊢\left(W\in \mathrm{LMod}\wedge X\in S\right)\to \left\{\underset{\dot{}}{0}\right\}\subseteq X$$

Proof

Step	Hyp	Ref	Expression
1		lss0cl.z	$$⊢\underset{\dot{}}{0}=0_W$$
2		lss0cl.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
3	1 2	lss0cl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in S\right)\to \underset{\dot{}}{0}\in X$$
4	3	snssd	$$⊢\left(W\in \mathrm{LMod}\wedge X\in S\right)\to \left\{\underset{\dot{}}{0}\right\}\subseteq X$$