Theorem lssle0

Description: No subspace is smaller than the zero subspace. ( shle0 analog.) (Contributed by NM, 20-Apr-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lss0cl.z	|- .0. = ( 0g ` W )
	lss0cl.s	|- S = ( LSubSp ` W )
Assertion	lssle0	|- ( ( W e. LMod /\ X e. S ) -> ( X C_ { .0. } <-> X = { .0. } ) )

Proof

Step	Hyp	Ref	Expression
1		lss0cl.z	|- .0. = ( 0g ` W )
2		lss0cl.s	|- S = ( LSubSp ` W )
3	1 2	lss0ss	|- ( ( W e. LMod /\ X e. S ) -> { .0. } C_ X )
4	3	biantrud	|- ( ( W e. LMod /\ X e. S ) -> ( X C_ { .0. } <-> ( X C_ { .0. } /\ { .0. } C_ X ) ) )
5		eqss	|- ( X = { .0. } <-> ( X C_ { .0. } /\ { .0. } C_ X ) )
6	4 5	bitr4di	|- ( ( W e. LMod /\ X e. S ) -> ( X C_ { .0. } <-> X = { .0. } ) )