This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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{˙}{0} = 0_{W}$
	lss0cl.s	$⊢ S = LSubSp (W)$
Assertion	lss0ss	$⊢ (W \in LMod \land X \in S) \to \{\underset{˙}{0}\} \subseteq X$

Proof

Step	Hyp	Ref	Expression
1		lss0cl.z	$⊢ \underset{˙}{0} = 0_{W}$
2		lss0cl.s	$⊢ S = LSubSp (W)$
3	1 2	lss0cl	$⊢ (W \in LMod \land X \in S) \to \underset{˙}{0} \in X$
4	3	snssd	$⊢ (W \in LMod \land X \in S) \to \{\underset{˙}{0}\} \subseteq X$